Information Technology Reference
In-Depth Information
1. The environment
s
c
is added to
Label
(
G
, x
), the label of state
x
.
2. Any environment from
Label
(
, x
) which is a superset of some other
environments in this label is deleted to ensure hypotheses minimality.
3. If
s
c
is still contained in the label of
x
then
t
is pointed to the predecessor
state
x
and
s
is appended to
G
U
B
.
The outcome of the three phases is a graph
of the potential scenarios that
lead to the collected evidences. It embodies different initial system states apart
from the ones described by the specification. In fact, in the context of forensic
investigation, an attack scenario could start from a legitimate system state, as
well as from a previous system incident or instability.
G
6
Case Study
To make concrete the use of S-TLA
+
and S-TLC in digital forensic investigation,
we propose this case study which is an investigation of a standalone (discon-
nected from network) system that is compromised, where an illegal privileged
access is detected. The system ran initially with two users accounts: a root and
an unprivileged user. A straightforward examination by experts shows that the
system security log is altered. The latter no longer contains more than a single
unexpected record showing that the system root has closed its session.
6.1 S-TLA
+
Specification Description
The following set of S-TLA
+
actions is specified to represent hacking scenarios
fragments. For the sake of readability, we ignore the fragments that will not be
part of the whole expected scenarios.
-
LogAsUsr
: Using the hypothesis stating that the user password is a well-
known word, an intruder guesses the password and gains access to the system,
raising its privilege
localpr
from 0 to 1. Moreover, the pair
is appended to the sequence
log
to log such event. Note that 0 means there
is no granted access, while 1 lets a user execute any non administrative
command. Finally, 2 refers to the root privilege.
LogAsUsr
“
usr
”
,
“
logon
”
∆
=
userhas
=
“weakpwd”
localpr
=1
∧
∧
localpr
=0
∧
log
=
Append
(
log,
)
-
InstSoft
: A user who gained an unprivileged access can install its own soft-
ware, particularly, a vulnerability exploit tool.
InstSoft
∧
“usr”
,
“logon”
addsft
=
“exploit”
-
ExpLclVuln
: Hypothesizing that there is a vulnerability in one of the installed
super-user commands that could grant a privileged access, if exploited, the
current user exploits such vulnerability and rises its privilege from 1 to 2.
The system kernel updates sequence
log
in order to log the event.
ExpLclVuln
∆
=
localpr
=1
∧
addsft
=
“”
∧
∆
=
∧
roothas
=
“vulnbin”
∧
localpr
=1
∧
addsft
=
“exploit”
localpr
=2
log
=
Append
(
log,
∧
∧
“root”
,
“logon”
)
