Information Technology Reference
In-Depth Information
and sound, but the criterion is undecidable, and for the best of our knowledge
no approximation has yet been implemented. Existing Java verification tools
that use standard JML [17] as a property specification language do not support
non-interference certification (see [2] for a further discussion). A flow-sensitive
and termination-insensitive analysis for object-oriented programs based on Hoare
logic is proposed in Amtoft et. al [3]. This analysis considers pointer aliasing that
can leak confidential information. The non-interference property is specified by
using independence assertions that are written in JML. In order to compute
postconditions, the analysis uses an algorithm that is sound and complete given
some assumptions, but it does not generate a program security proof.
Although non-interference has not been considered in current PCC implemen-
tations, there are some proposals that are based on type systems (see [2] for some
key references). However, none of these use JML to express non-interference poli-
cies and none of them have yet been implemented. In [16], Hunt and Sands pro-
pose a flow sensitive, dynamic type system that has not yet been implemented. It
tracks syntactical dependences between program variables in a simple imperative
language without objects or function calls [16]. Moreover, we have shown that
our analysis can achieve more precision than traditional, type-based approaches,
thanks to the combination of static analysis and dynamic labeling. Wasserrab et.
al present in [24] the first machine-checked correctness proof for information-flow
control that is based on program dependence graphs using static intraprocedu-
ral slicing. The proof is formalized in Isabelle/HOL. The analysis applies to
deterministic terminating programs and is flow-sensitive, object-sensitive and
context-sensitive. The machine-checked proof was instantiated for a simple im-
perative language with loops and for a subset of Jinja (a definition of Java byte-
code), which must be manually annotated with security labels. This work does
not consider method calls, classes, or objects. Bavera and Bonelli [6] present a
flow-sensitive type system for verifying non-interference of bytecode, where class
fields may have different confidentality labels for different instance objects. This
methodology does not consider method calls and it does not generate checkable
proofs. Moreover, as is usually the case in type-based analysis, once the object
fields and the variable labels are determined, they remain fixed throughout the
analysis. A proposal that deals with dynamic information-flow policies is [21].
This technique is based on runtime tracking of indirect dependencies between
program points. While our confidentiality label tracking is also dynamic, our
approach is based on static analysis rather than runtime monitoring, similarly
to [16,23].
Some proposals also exist for non-interference verification that are based on
abstract interpretation (see [26,25] and [2] for further references). However, these
proposals do not generate a certificate as an outcome of the verification process,
and they do not use JML to express non-interference policies. The idea of first
enriching the original semantics of the language by pairing each data value to its
security level, and then approximating it by only considering the security level
was also proposed in [4,26]. By using classes and class hierachies as abstract
domains, Zanardini adopts a different perspective of abstract non-interference
Search WWH ::




Custom Search