Information Technology Reference
In-Depth Information
is a simple non-interferent example borrowed from [16]. It is structured into two
classes. Program
3
includes three simple methods in two classes: one of which is
an interferent method borrowed from [23]. The main method has a sequence of
method invocations such that the last invocation calls a non-interferent method,
and thus the entire program is non-interferent. Program
4
includes six simple
methods, the three methods included in program
3
and three other interferent
methods also borrowed from [23], including a method with a
while
loop and a
method that calls another method. In this case, the last invoked method as well
as the whole example program are non-interferent. Similarly, program
5
includes
nine simple methods, the six examples included in program
4
plus three other
interferent methods: two interferent variations of the loop example of program
5
and an interferent method with a return statement within a conditional state-
ment. The source code of our benchmarks is provided within the distribution
package.
The experiments are very encouraging since they show that the reduction in
size of the certificate is very significant in all cases, with the quotient “
Red. Rules
Cert. Size/Full Cert. Size
” ranging from 0
.
54% in program
2
to 0
.
09% in program
5
. Note that the biggest reduction occurs for the largest program. When the time
employed to generate the full and reduced rules certificates are compared, the
reduced certificate generation time vs the full certificate generation time range
from 11
,
32% to 67
.
80%. The reduction for the biggest example (program
5
)was
the largest one (11
,
32%). Note that the generation time for the reduced labels
certificate were not significantly lower than the reduced rules certificate. These
results show that the technique scales up better when reduced certificates are
considered.
7 Related Work
Goguen and Meseguer [15] formalized non-interference of deterministic and ter-
minating systems as a system hyperproperty [7], i.e., a security property that
is defined for pairs of system output traces that are indistinguisable for an ob-
server. In [13], Foccardi and Gorrieri defined a stronger, security-based notion of
non-interference that considers pairs of system input/output traces. In contrast
to [13], our safety-based notion of strong non-interference only considers secret
outputs, similarly to [15].
Barthe et. al [5] develop a methodology to prove non-interference of determin-
istic terminating programs in an imperative language with loops, conditionals,
and mutable data structures (i.e. objects). Their methodology relyies on us-
ing Hoare logic and separation logic, and handles non-interference as a safety
property by using program self-composition with variable renaming (i.e., they
compose a program with a copy of itself without sharing memory positions).
Their method can verify non-interference of secure programs with temporary
breaches such as “
low
=
high
;
low
=
2
”, whereas imprecise conservative type
systems [22,26,4] cannot. Also, their method can deal with Examples 4 and 7,
whereas we cannot ensure security for the last example. This proposal is complete
