Information Technology Reference
In-Depth Information
-
If
t
n
does not exist in
, it is appended as a new node with a label equal
to
t
c
and a predecessor equal to
s
n
. Then,
t
is appended to
G
U
B
if it satisfies
EvidenceState
, otherwise it is attached to
U
F
.
-
If there exists a node
x
in
which is the same as
t
n
and whose label includes
t
c
, then a conclusion could be made stating that
t
has been added previously
to
G
. In that case, a pointer is simply added from
x
to
s
n
.
-
If there exists a node
x
in
G
that is the same as
t
n
, but whose label does not
include
t
c
, then the node label is updated in the following manner:
1.
t
c
is added to
Label
(
G
, x
).
2. Any environment from
Label
(
G
, x
), which is a superset of some other
environment in this label, is deleted to ensure hypotheses minimality.
Formally, an environment
E
1
is a superset of
E
2
in the same environment
iff:
E
1
(
x
)=
E
2
(
x
)
G
,where
E
(
x
)representsthe
x
th
∨
E
2
(
x
)=
∇
value in
,
1
,
3).
3. If
t
c
is still contained in the label of state
x
(meaning that it was not
deletedinstep(2))thennode
x
is pointed to
s
n
and node
t
is appended
to
E
. An environment (8
,
1
,
3) is for instance a superset of (
∇
U
B
if it satisfies
EvidenceState
. Otherwise, it is attached to
U
F
.
Every node label is provided with the following four properties: 1) Soundness:
anode
x
holds each environment
E
i
; 2) Consistency: None environment
E
i
in
Label
(
, x
) is inconsistent, preventing
Inc
from holding; 3) Completeness: every
environment
E
is a superset of some
E
i
; and 4) Minimality: no environment
E
i
is a proper subset of any other.
Forward chaining may generate many slices of global attacks scenarios, a
great majority of them are useless due to further occurrence of inconsistencies or
because they do not lead to evidence generation. Nevertheless, this may generate
additional source of evidences and show the propagation steps of the attack.
G
Backward Chaining Phase:
This phase helps obtaining potential and addi-
tional scenarios that could be the root causes for the set of available evidences.
This phase starts with
U
B
holding the set of terminal states; the ones that sat-
isfied
EvidenceState
in forward chaining phase. Afterwards, and until the queue
becomes empty, the tail of
U
B
, described by
t
, is retrieved and its predecessor
states (the set of states
s
i
such that (
s
i
, t
) satisfies action
Next
) which are not
terminal states and satisfy
Invariant
(States that do not satisfy
Invariant
are
discarded because this phase does not aim to check whether a specification is
correct or not but simply to generate additional explanations) and
Constraint
are computed. Each computed
s
is appended to
G
as follows:
-
If
s
n
does not exist in
,anewnode(setto
s
n
) is appended to the graph
with a label equal to
s
c
. Afterwards, a pointer is added from
t
n
to
s
n
and
s
is appended to
G
U
B
.
-
If there exists a node
x
in
which is the same as
s
n
, and whose label includes
s
c
,then
s
was added previously to
G
. In that case a pointer is simply added
from
t
n
to
s
n
and
s
is appended to
U
B
.
-
If there exists a node
x
in
G
which is the same as
s
n
, but whose label does
not include
s
c
, then the node label of
x
is updated in the following manner:
G
