Instance-Specific Security Domain Assignments 
in Sequential Programming Languages


Most commonly used programming languages support the instantiation of 
record data structures on a heap. Existing noninterference-based 
security conditions for such languages use security policies which 
assign security domains to the names of record fields. We demonstrate 
that security analyses enforcing such policies are too imprecise for 
practical use.

One approach to increasing the precision of security analyses for 
languages providing a heap is to enable the definition of more 
expressive security policies which can take into account how individual 
instances of a record are used in a program. We follow this approach 
and introduce security policies based on instance-specific assignments 
of security domains to fields. Furthermore, we define a notion of 
indistinguishability for configurations of programs with heaps based 
upon such assignments. We then define a novel termination-insensitive 
noninterference-based security condition, IS-security, in terms of the 
new notion of indistinguishability.

To demonstrate that the new security condition enables more precise 
security analyses, we present a security type system for the purpose 
of automatically certifying programs for IS-security. For this, we 
address the additional complexity which arises from the fact that 
instance-specific domain assignments are necessarily dynamic in nature. 
In particular, we propose a method of soundly reasoning about the 
dynamic security domains of fields as part of a static analysis, using 
the precomputed results of a pointer analysis of the program to be 
certified.