A Temporal Logic-Based Model for Forensic Investigation in Networked System Security - Computer Network Security - page 331

This is an unacceptable execution as it drives to a state where the S-TLA in-
consistency predicate Inc will be true. Besides, a successive execution of action
A followed by C is legitimate.

Computer Forensic Investigation Using S-TLA +

4.2

A scenario fragment component as modeled in Section 2 matches well the form
of a S-TLA + action. In fact, pre-conditions, generated hypotheses, and actions
which represent the context of a scenario fragment can be described respectively
by state-predicates, relations between assumed and non-assumed variables, and
relations between primed and unprimed variables.
A digital forensic evidence can take the form of a temporal property (e.g., a
hacked system is issuing every so often an outbound connection to send sniffed
passwords), or an undesirable state of a system component (e.g., an altered file
is a violation of the integrity property). These two forms can be specified in
S-TLA + using temporal formulas, and state predicates, respectively.
An expected hacking scenario is a disjunction of scenarios fragments (i.e.,
S-TLA + actions) denoting possible hacking events starting from a state repre-
senting a safe system and ending in a state satisfying the digital evidence(s). The
core S-TLA logic works by infinitely selecting the suitable scenario fragment that
copes with the attained system behavior, such that no inconsistency is holding
and composing it with the previous ones into potential hacking scenarios.

5 S-TLC: A Model Checker for S-TLA + Specifications

To automate the proof in the context of forensic investigation, we propose S-TLC
as an automated verification tool for S-TLA + specifications with a stress on the
handling of hypotheses and an improvement in the states space representation.
S-TLC is somehow an extension to the Model Checker TLC[6], which checks S-
TLA + specifications for errors such as silliness, invariance properties violation,
and deadlock [6-chapter 14]. In the following, we emphasize on the contributions
and changes in S-TLC, namely state computation and scenario inference.

5.1 S-TLC's States Space Representation

Given two different states that represent respectively a valuation ( x =1)of
the variable x under two possible sets of hypotheses ( h =1 ∧ g =2)and

( h =3 g = 3). Representing a state as a valuation of all its variables (as

in Figure 3) will involve a representation of two different states ((1 , 1 , 2) and
(1 , 3 , 3)) in the generated scenarios. We propose a more developed and optimal
representation involving two notions: node core and node label .Thecoreofanode
represents a valuation of the entire non-constrained variables, and the node label
represents the potential sets of hypotheses (a set of hypotheses is a valuation
of the entire constrained variables) under which the node core is reached. The
node label is represented and maintained in a way akin to the one used in the

∧