Information Technology Reference
In-Depth Information
-
ChangeID
: Hypothesizing that the root password is equal to the user's, the
user changes its identity to the root by providing the correct password. Con-
sequently, its privilege rises from 1 to 2, and the event is logged.
ChangeID
∆
=
roothas
=
“pwdequser”
localpr
=2
∧
∧
localpr
=1
∧
log
=
Append
(
log,
∧
“root”
,
“logon”
)
-
ExtSoft
: Given a software installed on the system for security auditing pur-
pose, the user copies one binary command from those that come with it to
be used maliciously as an exploit tool.
ExtSoft
∆
=
localpr
=1
addsft
=
“exploit”
∧
addsft
=
“audittool”
∧
-
CleanLog
: A privileged user can clean the log file content.
ClaenLog
∆
=
localpr
=2
log
=
∧
log
=
∧
-
DelSoft
: A privileged user can delete the whole tools unexpectedly installed.
delSoft
∆
=
localpr
=2
addsft
=
“”
∧
addsft
“”
∧
-
Exit
: The user logs off, its privilege goes down to 0 and the event is logged.
Exit
∆
=
localpr
=
localpr
=0
log
=
Append
(
log,
∧
∧
“root”
,
“logoff”
)
Inconsistency defined as:
userhas
=”
weakpwd
”
roothas
=”
pwdequser
”
,
states
that a system state should not be reached under a conjunct of the following two
hypotheses: a) the user password is a well-known word and b) the root password
is equal to the user one. In fact, the forensic investigator is sure that the root
password fulfills a strong password policy. The available evidence is described by
predicate
EvidenceState
∧
∆
=
Head
(
log
)=
”
root
”
,
”
logoff
”
, which states that
the finite sequence
log
encloses only one record equal to
.
The system under investigation is specified by a S-TLA
+
formula
Spec
simi-
larly to the form described in section 4.1, where
Init
describes the initial system
state (empty log file, no unexpected tool installed, no granted access).
Init
“
root
”
,
“
logoff
”
∆
=
localpr
=0
∧
log
=
∧
addsft
=
“”
∧
userhas
=
∇∧
roothas
=
∇
6.2
Investigation Using S-TLC
Figure 4 describes the results generated by S-TLC until the forward chaining
phase. It outlines two different system states (the ones which are encircled)
satisfying predicate
EvidenceState
, where one of them shows a new generated
evidence as an exploit tool installed by the malicious user to exploit a local
vulnerability. These two evidences can be generated under two possible set of
hypotheses: 1) the user password is weak and one of the installed system com-
mands contains a vulnerability that grants a privileged access; and 2) the user
password and the password hashing algorithm are both weak. Two main possible
scenarios may be distinguished in this phase:
1. An intruder guesses the weak user password and gains an unprivileged access.
Afterwards, it exploits a weakness in the password hashing algorithm and
