Information Technology Reference
In-Depth Information
rl k(LVal -> (if(S,S') -> K)) lenv(CL) => k(S -> K) lenv(CL join LVal).
rl k(LVal -> (if(S,S') -> K)) lenv(CL) => k(S' -> K) lenv(CL join LVal).
Fig. 8. Abstract rules for the if-then-else
alternatives in a non-deterministic way. By abuse, we denote the abstraction of a
rule α (
{
l
}
)
α (
{
r
}
)by α (
{
l
}→{
r
}
).
P Java denotes the sort of Java programs
P Java (i.e. P Java ∈P Java ).
Java #
Definition 4 (Abstract rewriting). We define abstract rewriting
( State E ))
( State E )) by
P Java ×
×
P Java ×
P Java 1 ,SSt 1 Java #
P Java 2 ,SSt 2
(
(
if ∃u ∈ SSt 1 ,
v
SSt 2 s.t.
P Java 1 ,u
Java E
P Java 2 ,v
.
Java # the extension of
We denote by
Java # to multiple rewrite steps.
( State E )
P Java ,St 1 Java E
St 2
Lemma 2. If
, then there exists SSt 3
St 1 }
Java #
and St 2
s.t.
P Java (
{
)
SSt 3
SSt 3 .
A program is non-interferent for a given labeling function if the abstract values
(the confidentiality labels) of the Low variables in the final state of an abstract
program execution do not have the label Low High .
Theorem 2 (Abstract Non-Interference Soundness). GivenaJavapro-
gram P Java , P Java is non-interferent (Definition 2) if for all SSt 1
( State E )
Java #
s.t.
P Java ,SSt 1
SSt 2
, for all St
SSt 2 ,andforallvariables
var
Low ( P Java ) , St [ var ]=
Val, Low
for a value Val .
The following example illustrates the mechanization of the Java non-interference
analysis.
Example 8. Consider again the Java program of Example 1. By virtue of the
abstraction, we consider just one abstract initial state that safely approximates
any extended initial state and compute the corresponding abstract final states.
search in PGM-SEMANTICS-ABSTRACT :
java((preprocess(EX1-MAUDE) noType . 'main < new string [i(0)] > noVal))
=>! M:Store .
Solution 1 M:Store --> store([l(6),Low >> High] ...)
No more solutions.
Due to the transformation of some equations into rules in the abstract semantics,
there may be several execution paths but all lead to the same abstract final state.
6 Experiments
Our methodology generates a safety certificate which essentially consists of the
set of (abstract) rewriting proofs that implicitly describe the program states
which can (and cannot) be reached from a given (abstract) initial state, as il-
lustrated in Example 8. Since these proofs correspond to the execution of the
 
Search WWH ::




Custom Search