Symbolic Abstract Heaps for Polymorphic Information-flow Guard Inference(Extended Version)

Nicolas Berthier

University of Liverpool

Narges Khakpour

Newcastle University

Linnæus University
Newcstle upon Tyne

Nicolas Berthier1 Narges Khakpour2

OCamlPro (France), University of Liverpool (UK)

Newcastle University (UK), Linnæus University (Sweden)

In the realm of sound object-oriented program analyses for information-flow control, very few approaches adopt flow-sensitive abstractions of the heap that enable a precise modeling  of implicit flows.
To tackle this challenge, we advance a new symbolic abstraction approach for modeling the heap in -like programs.
We use a store-less representation that is parameterized with a family of relations among references to offer various levels of precision based on user preferences.
This enables us to automatically infer polymorphic information-flow guards for methods via a co-reachability analysis of a symbolic finite-state system.
We instantiate the heap abstraction with three different families of relations.
We prove the soundness of our approach and compare the precision and scalability obtained with each instantiated heap domain by using the benchmarks and real-life applications.

Information flow control,  heap abstraction, language-based security, static analysis, low-level code

Security and privacy

§ INTRODUCTION

Information Flow Control (IFC) mechanisms offer an effective approach to
prevent unwanted disclosure of confidential information, or illegal tampering of data.

Their task is to ensure confidentiality and/or integrity, which are usually formalized as noninterference baseline properties [Goguen and Meseguer, 1982].

Confidentiality demands that high-sensitive (secret) inputs do not influence low-sensitive (public) outputs.
This means that any change in the value of a secret input must not induce a change in any public output.
In other words, there must be no information flow from any secret
to any public output.
In software programs, information may flow explicitly via direct assignments, from y to x in @x = y;@, or implicitly when the execution of statements is guarded by a condition, from c to x in @if (c > 0) x =<EMAIL_ADDRESS>
Many static analysis approaches to ensure noninterference have been advanced, that rely on type-systems [Pottier and Simonet, 2003, Sabelfeld and Myers, 2003, Barthe et al., 2007, Liu and Milanova, 2010, Hedin and Sabelfeld, 2012], self-composition [Barthe et al., 2011, Terauchi and Aiken, 2005, Barthe et al., 2011], theorem-proving [Darvas et al., 2005], and abstract interpretation <cit.>.

Flow-insensitive static analyses (with “flow” as in “control-flow”) deal with a single set of facts that is valid for all possible executions of the whole program

, whereas flow-sensitive analyses

provide one set of facts for each statement.
In general,

flow-sensitivity increases precision, yet

comes with an additional computational cost.
Heap abstractions as computed by alias or points-to analyses obey the same principle
[Kanvar and Khedker, 2016]: a flow-insensitive heap analysis provides a single, finite representation of the conceptually infinite set of memory locations manipulated by all entire executions of the program, while a flow-sensitive variant gives an abstraction of the heap at each statement.

Note that a flow-sensitive analysis for object-oriented programs may rely on a flow-insensitive heap abstraction; this means that the analysis must remain imprecise when dealing with heap-allocated structures.

We consider a -style low-level object-oriented language whose syntax is close to 's [Vallée-Rai et al., 2010],
and design a static IFC analysis that automatically decides whether a program \(P\) implemented in this language is secure, \(P\) satisfies a desired noninterference property.
Several approaches have been proposed to verify such properties for -style languages [Barthe et al., 2007, Hammer and Snelting, 2009, Liu and Milanova, 2010, Gordon et al., 2015, Arzt et al., 2014, Johnson et al., 2015, Lortz et al., 2014, Darvas et al., 2005, Zanioli et al., 2012].
To the best of our knowledge, however, none of the sound and scalable solutions rely on a flow-sensitive heap abstraction.

Our analysis is therefore the first of its kind, as it is sound, shows potential for scalability since it supports modularity,
and both:

* captures implicit flows; and

* relies on a flow-sensitive heap abstraction.

Achieving these goals in combination is challenging because

the analysis must
track the information flows that result from

manipulations of object fields and references performed in the program branches that are taken as well as in any program branch that is not taken: it must therefore reflect about the states of the heap in both taken and non-taken branches  simultaneously.

[yep]The only work we have found that does consider implicit flows with a flow-sensitive heap abstraction was developed by Zanioli et al., 2012

; it however only operates intra-procedurally and on high-level structured programs.

To do so,

we use a security typing environment that associates each memory location manipulated by the program \(P\)
with a security level.

In the case of confidentiality, such a level indicates whether the memory location may hold high-sensitive (secret) data, and \(P\) is secure if

no value from a high-sensitive source

flows to a sink statement.

To deal with all information flows in the heap, we introduce the notion of symbolic abstract heap domains, that combine a flow-sensitive security typing environment for every object reachable from a given set of reference variables \(R\), with a flow-sensitive representation of a set of heap-related relations pertaining to \(R\) (aliasing).
The domains are parametric in a family of heap-related relations, which defines the relations that are captured flow-sensitively by the domain.
allows us to define multiple heap abstractions, each one with its level of precision.
Abstract heaps in such a domain are predicates in a propositional logic, that provide a store-less model of the heap where irrelevant details related to the behaviors of the memory allocator and garbage collection are safely abstracted away.
The semantics of reference and object mutations are specified using predicate transformers.

These can be used to encode the security semantics of any method \(m\) of the program by means of a symbolic transition system \(S_m\),
where the desired noninterference property is reduced to a safety property \(φ_m\) [Boudol, 2009]

[yep]We construct our symbolic abstraction based on a store-less model of the heap that provides us with canonical representations for semantically equivalent heap graphs (up to isomorphismthis probably needs reformulation), and where irrelevant details related to the behaviors of the memory allocator and garbage collection are safely abstracted away.
[yep]Our construction relies on a simplified variant of the store-less structures developed by <cit.>, where we distinguish every set of reachable objects as equivalence classes defined using heap-related relations among reference variables, instead of more complex symbolic access paths.

Artifacts that we can infer for a method \(m\) include an information-flow guard, that is a predicate expressed on propositional “facts” about security levels and heap-related relations pertaining to \(m\)'s formal arguments.
This guard describes (sufficient) circumstances upon which \(m\) is secure, and it is polymorphic since it is valid in any calling context.
More elaborate artifacts that additionally describe the effects of \(m\) on the heap enable sound inter-procedural analyses.
In the present paper, however, we focus on our approach for abstracting the heap
and concentrate our exposition on the inference of
guards; we leave the inference of polymorphic effects for a future publication.

We compute the guard for a method \(m\) via a co-reachability analysis of the system \(S_m\) its safety property \(φ_m\). A co-reachability analysis finds all states from which a given set of states may be reached, and is typically solved using a fixed-point [Ramadge and Wonham, 1989, Pnueli and Rosner, 1989].

We have implemented the guard inference algorithm in a prototype tool called , available at <http://nberth.space/symmaries>, that is equipped with several instantiations of symbolic abstract heap domains using various families of heap-related relations.

§.§.§ Summary of Contributions

* We introduce a novel notion of symbolic abstract heap domains that

uses a set of relations to represent the heap, and is the first flow-sensitive heap model used for information-flow control analysis.
We define three different instances of this domain (, , ), each with a different set of relations (Section <ref>), and show that constitutes a secure heap abstraction (Section <ref>);

* We symbolically specify the security semantics of our input language to capture explicit and implicit flows via the heap, and infer polymorphic information-flow guards via a co-reachability analysis (Section <ref>).
We prove that our analysis under a secure heap abstraction guarantees termination-insensitive noninterference [Sabelfeld and Myers, 2003];

* We
empirically study the respective impacts of our three heap domains, in terms of precision on benchmarks [Hamann et al., 2018], and in terms of scalability with 60 real-life ABM applications [Do et al., 2016]
(Section <ref>).
Our experiments show that our approach offers the best precision, and the heap model precision has an inverse relationship with scalability. The heap domains and , that are resp. the least- and most-precise heap model, improve the state-of-the-art precision by 2.4% and 4.2% respectively.

* While the existing approaches use an (flow-insensitive) heap model, offers six different heap models, thereby allowing the user to choose a suitable heap model based on her preferences for precision and scalability.

§ PRELIMINARIES

§.§.§ Input Programs

The signature of a method consists in a tuple \(\MethSign{} ≝ 〈\MethClass{}, \MethFormalArgs{}, \MethRet{}〉\) where \(\MethClass{} ∈ \Classes\) is the name of its enclosing class, \(\MethFormalArgs{}% : （\Variables ∪ ｛\this｝） ⇀ （\PrimTypes ∪
% \Classes）
\) is a mapping from each formal argument to its respective type, and \(\MethRet{} ∈ \PrimTypes ∪ \Classes ∪ ｛\void｝\) is its return type.

We consider a -style low-level language where the code of a

\[
\begin{array}{r@{\ }r@{\ }l}
\stms &⩴& [\lbl{lbl}:]~\stm;\stms \sep \surd \\
\stm &⩴& v = e \sep v = r.f_p \sep r.f_p = e \\
&|& r = r \sep r = r.f_r \sep r.f_r = r \\
&|& r = \cnew~c \sep r = \Null \sep r.m(\lits)\\
%	    &|& v = r.m(\lits) \sep r = r.m(\lits)  \sep r.m(\lits)\\
&|& \cgoto~\lbl{lbl} \sep \cif~(e)~\cgoto~\lbl{lbl} \\
&|& \coutput l (v) \sep \coutput l (r) \\
%	    	&|& \creturn~ [v \sep r]
%	    	\\
e &⩴& p \sep v \sep ⊖ e \sep e ⊕ e \sep r == r \\
\end{array}
\]

method is a non-empty finite semicolon-separated sequence of statements built according to in the grammar on the right, where square brackets denote optional constructs.
\(\surd\) is an empty sequence of statements, and \(\lbl{lbl} ∈ \Labels{}\) is a label that uniquely identifies a statement.
\(c %∈ \Classes
\) is a class name, \(f_p\) (resp. \(f_r\)) is a primitive (resp. reference) field name, \(p\) is a scalar constant, and \(e\) is an expression.

\(v\) (resp. \(r\)) depicts any local primitive (resp. reference) variable or formal argument used of the method in .
[yep]; we use \(x\) to denote any such variable

\(\coutput{l}(v)\) sends data $v$ over a channel with the security label \(l\). The label $l$ belongs to a two-level security domain which is
formalized as a
lattice \(〈\LL, ⊑, ⊔%, ⊓
〉\), where $\LL=\{⊥, ⊤\}$ is the set of security levels, $\low$ is the low-sensitive label, $\high$ is the high-sensitive label, \(⊑\) is a partial order defined over with \(⊥ ⊑ ⊤\), and ⊔ gives the least-upper-bound
As is traditional, we will present our work by focusing on a standard two-level lattice \(\LL ≝ ｛⊥,⊤｝\); minor adaptations would be necessary to support more complex lattices.].

Information may become public via sink statements, that we denote  $\coutput{⊥}(x)$.
Therefore, \(\coutput{⊥}(v)\) is a sink for the value of \(v\), and \(\coutput{⊥}(r)\) is a sink for every object that is reachable in the heap via the reference \(r\).

§.§.§ Symbolic Control-flow Graphs — SCFGs

The transition systems that we use to encode the security semantics are
traditional labeled transition systems augmented with sets of state and input variables, respectively denoted \(X\) and \(I\).
The values for input variables can be seen as coming from the environment of the system.

A symbolic control-flow graph is a tuple \(S = 〈Λ, X, I, Δ, ℓ_0, X_0〉\) where:

Λ is a finite non-empty set of locations;

X and \(I\) respectively denote state and input variables;

Δ is a set of transitions labeled with a guard that is a predicate on state or input variables, and a possibly empty set of assignments to state variables, noted \([v_0 \assign e_0, …, v_n \assign e_n]\), or ∅ if empty;

ℓ_0 ∈ Λ is the initial location; and

X_0 is a predicate that describes the entire set of possible initial valuations for all the state variables.

Predicates and right-hand-side expressions in assignments are built using traditional logical connectives (¬, ∨, ∧ and ⇒), along with a ternary conditional construct “⋅⋅⋅” with an obvious meaning.

The symbolic variables we make use of typically take their values in the security domain , or the set of Booleans \(\BB ≝ ｛\ff, \tt｝\)

We use a merge operation to merge variable assignments
This operation is obtained as a union where multiple expressions assigned to a variable \(v\) are combined using some
connective \(⊔_v\).
The latter depends on the semantics of each variable:
as we only use variables to hold over-approximations in our encoding, we use the disjunction ∨ for Booleans, and the least-upper-bound ⊔ for security levels.
For instance, \(\{a \assign \tt, b \assign \ff\} \SQMergeiu \{b\assign \tt\} = \{a \assign \tt, b \assign \ff ∨ \tt\}\).
An invariant \(φ %: Λ → \PDomX{X}
\)
for the SCFG \(S\) is a mapping from locations to predicates on state variables.
\(S\) satisfies \(φ\) iff every state \(
%=(ℓ,x) % ∈ \Q_S
\) with location ℓ that is reachable by S is such that \(
⊨ φ
\).

An SCFG \(S\) induces a model S that is a finite-state automaton whose state-space \(\Q_S\) is the Cartesian product of the set of locations Λ and the set of all possible valuations for the state variables, \(\Q_S = Λ × \Val X\), where X is the set of valuations for all variables in \(X\).
S takes one transition whenever it receives a valuation for all the input variables, an element in I (an empty set for ).
In any location, there is always exactly one transition whose guard is satisfied by the valuations for all the variables.
When this transition is taken,

its assignments are applied to update the state variables.
In this work, we only construct SCFGs that are both deterministic and reactive: given any location \(ℓ ∈ Λ\) and valuations for input and state variables
, there always exists a unique transition in \(Δ(ℓ)\) whose guard is satisfied.
The only source of non-determinism that we make use of in the models lies in the sets of initial values for the state variables

Note there is also no notion of accepting state; combined with the properties above, this means that every infinite sequence of elements in I leads to a valid run

§ SYMBOLIC ABSTRACT HEAP DOMAINS

We first detail our design of heap abstractions that are suitable for the symbolic encoding of security semantics.
In this approach, one predicate is used to model a set of symbolic heaps.
Each symbolic heap represents a parameterizable set of heap-related relations between the portions of the heap that are reachable via a given set of references \(R\), along with a security typing environment for every reachable portion of heap.
Such predicates provide storeless representations since object locations are not explicitly represented.
Predicate transformers describe the effects of heap and reference variable mutations on sets of symbolic heaps.

§.§ Families of Heap-related Relations

Our definition of symbolic abstract heap domains is parameterized by

a family of heap-related relations.
A typical example of a heap-related relation is the aliasing relation, that we denote with the symbol , and which is defined as an equivalence relation where \(\AliasRel r s\) holds iff \(r\) and \(s\) point to the same object.

We define a family of heap-related relations
as a pair \(\hd ≝ 〈\HeapDomRelations, \HeapDomConstRelations
%, \TypeAnalysis R {}
is a set of flow-sensitive relations, and are constant flow-insensitive relations (or facts).
A relation
is formally specified as a set of Boolean variables that each indicates whether two  references taken from \(R\) are in the relation or not (we use predicate abstraction where a Boolean variable specifies whether a relation between two  references holds).
For instance, we need four propositions (therefore, as many Boolean variables) to represent the relation   defined over $R=\{a,b\}$, $\GenericRelVar[] a a$, $\GenericRelVar[] a b$, $\GenericRelVar[] b a$ and $\GenericRelVar[] b b$. The proposition $\GenericRel x y$ evaluates to true if $x$ is in the relation  with $y$. Further, a relation $\GenericRel{}{} =\{(a,a),(b,a)\}$ is formalized as $\GenericRelVar[] a a ∧ ¬ {\GenericRelVar[] a b} ∧ \GenericRelVar[] b a ∧ ¬ \GenericRelVar[] b b $.

The propositions about flow-sensitive relations may be updated by the program statements,

while the propositions about constant flow-insensitive relations are straightforwardly substituted with or ,

and serve the sole purpose of improving the precision of the predicate transformers that manipulate symbolic abstract heaps.
For instance, in a heap domain that does not handle the aliasing relation flow-sensitively,
two references of incompatible types can never alias each other.

We formalize this with the pre-analysis function R

, that returns three-valued sound
facts about the relations in = $\cup$
the set of reference variables \(R\).
Given any relation \(\GenericRelSymb ∈ \Rels\) and a pair of references \((r,s) ∈ R^2\),
R r s returns if r s always holds, if it cannot hold, or otherwise.
In its most trivial form, this pre-analysis function operates on a purely lexical level, by returning if queried for r r with a reflexive relation, otherwise.
It may additionally involve an analysis of the class hierarchy and take the declared type of the reference variables into account to give more precise facts.

Note that   helps us simplify the heap formulae by reducing the number of propositions used to represent heaps
. For instance, if $\GenericRel{}{}$ is a reflexive relation in our previous example, we don't need to consider the propositions a a and b b, and use the constant instead.
We leave further specifications of the pre-analysis open for the sake of modularity.

We need to differentiate between “flow-sensitive heaps” and “flow-sensitive heap relations”. The first case means that the heap changes during the execution while the latter states that the relation used to specify the heap structure changes during the execution (). Therefore, a flow-sensitive symbolic heap abstraction models at least one heap relation flow-sensitively.

§.§ Symbolic Abstract Heap Domain

Formally, a symbolic abstract heap domain for the family of heap-related relations
is defined as a pair $\SymbolicAbstractHeapDom R ≝ \langle
\HeapDom \hd , \Transformers \hd \rangle$
is the set of symbolic abstract heaps,
and is a set of predicate transformers to manipulate the abstract heaps.
A symbolic abstract heap from this domain
is a predicate \(\HeapPredicate[\sHeap] ∈ \HeapDom \hd\)
defined on two sets of state variables

and .

The set associates a security level variable [] r with each reference \(r ∈ R\), that represents an upper bound on the security levels of any object that is reachable via \(r\): these variables constitute the security typing environment for the abstract heap .

In turn, the set consists of Boolean variables that describe over-approximations of flow-sensitive heap-related relations between the references in \(R\),
a variable \(\GenericRelVar r s ∈ \GenericRelVars[\sHeap]\)
holds whenever \((r, s)\) may be in the heap-related relation :

\[\red{\GenericRelVars[\sHeap] ≝
｛\GenericRelVar r s ｜ (r,s)∈R^2, \GenericRelSymb ∈ \HeapDomRelations, \TypeAnalysis R {\GenericRel r s} = \TAmaybe ｝\mbox.}
\]

Further, and are sets of constants that capture all relations that never hold and always hold according to the function R , respectively.
(For the sake of readability, we will omit the exponent of security-level variables when a single abstract heap is involved, [] r will be denoted [] r.)

\begin{align*}
\GenericRelUnsat ≝
&\ ｛\GenericRelConst r s % ⟼ \ff
｜ \begin{array}{@{}l@{}}
\GenericRelSymb ∈ \HeapDomRelations ∪ \HeapDomConstRelations, \TypeAnalysis R {\GenericRel r s} = \TAunsat
\end{array}%
\\
\GenericRelTauto ≝
&\ ｛\GenericRelConst r s % ⟼ \tt
｜ \begin{array}{@{}l@{}}
\begin{array}{@{}l@{}}
（\GenericRelSymb ∈ \HeapDomRelations, \TypeAnalysis R {\GenericRel r s} = \TAtauto） ∨ \\
（\GenericRelSymb ∈ \HeapDomConstRelations, \TypeAnalysis R {\GenericRel r s} ≠ \TAunsat）
\end{array}%
\end{array}%
\end{align*}

[yep]can be written in full disjunctive normal form using \(N\) conjuncts as

\begin{equation*}
\label{eq:symbolic-abstract-heap-value-predicate}
\HeapPredicate =%
⋁_{i∈｛1,…,N｝}{（⋀_{\HLvl[\sHeap]r ∈ \GenericHLvlVars}{\HLvl[\sHeap]r = l_r}\ ∧
⋀_{\GenericRelVar r s \in \GenericRelVars}\boxed{\GenericRelVar r s}）}\mbox,
\end{equation*}

Maybe use inline text description for conciseness.

where \(l_r ∈ \LL\) is a security level for \(r\), and \(\boxed{e}\) can be either $e$ or its negation $\neg e$.

This form highlights that an abstract heap represents a set of symbolic heaps, each of which features a typing environment encoded with variables in the left-hand side of the conjunction.

We give the definitions of , and in  <ref>.
The former set encodes unknown or non-constant elements of the relations in using variables,
whereas symbols in the latter are conservatively defined according to the pre-analysis R .
Note that some symbols in may represent relations from that cannot be safely ruled out by the pre-analysis.

We summarize in  <ref> the main denotations that we use to represent and manipulate symbolic abstract heaps.
The leftmost column shows the variables that represent security levels and heap-related relations, along with the operator \(\HeapInit[\sHeap]{R'}\).
The right-hand side column

lists the set of predicate transformers that can be applied on a symbolic abstract heap to alter its representation.
The two first transformers in the column operate in accordance with a given reference assignment (\(\mathit{as}\)) or mutation (\(\mathit{mu}\)).
The expression \(l\) given to the latter gives the security level of the information that flows to mutated objects.

We give in  <ref> the definitions of all transformers
These definitions make use of
functions specialized for each family of heap-related relations, detailed below.
\(\HeapInit[\sHeap]{R'}\) builds a predicate that constrains variables in and to account for the fact that
a given set of references \(R'⊆R\)
—this notably entails that every object reachable via \(R'\) is low-sensitive.

The bulk upgrade is a transformer used to capture implicit flows through the heap by joining two distinct heap abstractions and \(\sHeap'\) that belong to the same domain.
More specifically, this transformer assumes that \(\hlvlH[\sHeap']r ⊑ \hlvlH[\sHeap]r\) for all \(r ∈ R\), and:

* copies the heap-related relations from \(\sHeap'\) to \(\sHeap\); and

* upgrades the typing environment of via a pairwise join with the corresponding levels in \(\sHeap'\).

Consider method @m@ given in  <ref>.
<ref> shows its references $R$, heap-related relations , references security levels and variables to specify the heap structure using relations . Further, the table in this Figure shows the heap transformers associated with each statement to update the heap relations and reference security levels.
As an example transformer, consider

that corresponds to the statement @r = new<EMAIL_ADDRESS>
With a heap domain that captures the aliasing relation flow-sensitively, the resulting set of assignments includes (at least) \(［\cAliasRel[\sHeap] b r \assign \ff, \chlvl[\sHeap] r \assign l］\) where \(l\) is a security level expression \(l ⊒ \pc\).

Further assuming that \(\sHeap ∧ \pc = ⊤\) holds on location \(ℓ_0\), then \(\chlvl[\sHeap] r = ⊤ ∧ ¬\cAliasRel[\sHeap]b r\) must hold on location \(ℓ_1\), which notably means that some object reachable via r might be high-sensitive after the object allocation (since
the allocation happens in high context).

Assuming the same domain as above for ,
\(X_0\) implies a predicate
\(\sHeap_0 = (\chlvl[\sHeap] r = ⊥ ∧ ¬\cAliasRel[\sHeap] b r)\), which represents the set of all heaps where every object reachable via r is low-sensitive, and b does not alias r.
Neither [] a nor [] b are bound in \(\sHeap_0\), which means that \(\sHeap_0\) represents an abstract heap
where no fact is known about the security levels of the sets of objects reachable via a or b.

Note, however, that if []b r were to hold, then we would need to ensure that \(\chlvl[\sHeap] b = \chlvl[\sHeap] r\) also holds.  More generally, we also want transitive (resp. symmetric, etc) relations to be represented as such by the relation variables.  Such well-formedness constraints
are invariants that must be maintained by the transformers

[Class definitions and method m.]

[Invariant \(φ_{\cv m}\).]

\(φ_{\cv m}(ℓ_3) ≝ \pc ⊔ \cplvl b ⊔ \chlvl[\sHeap] b = ⊥%  \red{∪}\\
% & \red{｛ℓ_i ⟼ \tt｝_{i∈\{0,1,2,3,5\}}}
\)

[SCFG .]

Method that manipulates references, with a representation of the corresponding SCFG and invariant.  Unneeded variables involved in modeling branching behaviors and capturing implicit flows have been omitted from \(X\), \(I\), and \(X_0\) for clarity

§.§ Instances of Symbolic Abstract Heap Domains

Example families of heap-related relations

{, }

{, }

We present three instances of the
domain introduced above.
We first define the transitive “field-aliasing” relation, denoted with the symbol ,

which states for any given pair of references \(r\) and \(s\), r s holds whenever a reference field of an object reachable via \(r\) is an alias of \(s\).

This relation allows heap domains to capture some useful facts about the structure of the graph of objects when it comes to maintaining object types such as security levels.

[yep]We also combine aliasing and field-aliasing to form
the “connecting” equivalence relation, denoted with the symbol .
This relation is such that r s holds whenever the object pointed to by \(s\) is also reachable via \(r\), or the converse: \(\ConnectRel r s ≝ \AliasRel r s ∨ \FieldAliasXRel r s ∨ \FieldAliasXRel s r\mbox.\)
This latter relation is inspired by the pointer interference analysis of <cit.>, whose goal is to find groups of references that point to the same overall data-structure
A domain that captures this relation basically associates the same security level with every object of such data-structures.

Variables and constants involved in representing when analyzing m, for each domain.
exponents have been omitted for readability.

3 D {a, b, r}

{b r, b a, r a}
{b r}

3 D {a b, a r, a a, a b, a r, b b, b r, r b, r r}

{a a, b b, r r}
{a a, b b, r r,b a, r a}
{a a, b b, r r,b r, b a, r a}

We now assume a sound pre-analysis function  over \(\{\AliasRelSymbol, \FieldAliasXRelSymbol\}\), and use the above relations to define the three families of heap-related relations based on which we shall instantiate our symbolic abstract heap domains:

[] R, with
\(\hdeep ≝ 〈\{\AliasRelSymbol, \FieldAliasXRelSymbol\}, ∅
%, \TAbase{}{}
〉\), uses symbolic variables to represent over-approximations of
aliasing and field-aliasing relations

[] R, with
\(\hshal ≝ 〈\{\AliasRelSymbol\}, \{\FieldAliasXRelSymbol\}%, \TAbase{}{}
only maintains a flow-sensitive over-approximation of the aliasing relation,

yet makes use of

field-aliasing facts to improve the precision of transformers;

* [] R, with \(\hdumb ≝ 〈∅, \{\AliasRelSymbol, \FieldAliasXRelSymbol\}%.\TAbase{}{}

does not represent any flow-sensitive heap-related relation,

yet makes use of flow-insensitive (field-)aliasing

* The symmetric deep-aliaing abstract heap domain is defined solely using the connecting relation with \(\hsyma ≝ 〈\{\ConnectRelSymbol\}, ∅, \TAsyma{}{}〉\), where
is straightforwardly defined based on  as

\begin{equation*}
\TAsyma R {\ConnectRel r s} ≝
\begin{cases}
\TAtauto &\!\!\text{if }⋁_{q∈\mathrm{rl}(r,s)}{\TAbase R {q} = \TAtauto} \\
\TAunsat &\!\!\text{if } ⋀_{q∈\mathrm{rl}(r,s)}{\TAbase R {q} = \TAunsat} \\
\TAmaybe \text{~~otherwise}\span
\end{cases}
\end{equation*}

where \(\mathrm{rl}(r,s)≝\{\AliasRel {r\,} {\,s},\FieldAliasXRel r s, \FieldAliasXRel s r\}\).

Consider method @m@ given in  <ref>,

and assume a class hierarchy pre-analysis.
We instantiate the three symbolic abstract heap domains as R and define an abstract heap
\(\sHeap ∈ \HeapDom \hd \), for each \(\hd ∈ ｛\hdeep, \hshal, \hdumb% , \hsyma
<ref> shows the sets of variables used by each one of these domains to represent (and ), along with the symbols that denote constants
involved in
capturing relations flow-insensitively (and ).

[“Instantiating” ]

Assume a set of reference variables \(R = \{\cv r, \cv s\}\), and that any object pointed to by \(\cv s\) may only contain primitive fields—no field of s may point to any object, thus we can always assume \(\cFieldAliasXRel{\cv s}{\cv r} = \cFieldAliasXRel{\cv s}{\cv s} = \ff\).
We construct the abstract domain with \(\DeepHeapAbstractDom R = 〈R, \HeapDomRelations, \DeepHeapDom R, \DeepTransformers R〉\).
Let ∈ R be an abstract heap
from this domain.
Then,  is a predicate built using the variables [] r, [] s, [] r s, [] r r, and [] r s.

Regarding transformers, we give in  <ref> the specialized functions used by their definitions in  <ref>

The domains defined with \(\hd ∈ ｛\hdeep, \hshal, \hdumb｝\) share these definitions.

r updates relation variables in to reflect the erasing of a given reference \(r\) to either or a fresh reference by clearing variables from []
In turn, r s updates the variables in to encode the copy of a reference \(s\) to \(r\).

\(\GenericHeapLoadRef r s {f_r}\) makes any reference \(d\) that may be an alias of one of \(s\)'s field a potential alias of \(r\) (when a corresponding variable [] d r belongs to []), and updates any variable that
represents the relation to reflect that \(s\) becomes a field-alias of \(r\).

\(\GenericHeapStoreRef r {f_r} s\) makes \(s\) a field-alias of \(r\) while maintaining transitivity of .
Storing a reference may only add elements in relation , hence the disjunction in every assignment defined by this operation.

Observe that, as can be seen in the definition of r s f_r for \(\hd = \hshal\),

instead of simply setting \(\AliasRel d r \assign \tt\) for every potential alias \(d\) of \(r\) (blindly assuming that no information is known about the potential aliasing relation), a constant s d \(∈ \GenericRelTauto ∪ \GenericRelUnsat\) is used instead to further restrict the new potential aliases to the cases that have not been ruled out by
the pre-analysis.
The domain involves some pre-established facts via a similar mechanism.

\(\GenericUpgradeObjLevel r l\) takes a reference \(r\) and a security level expression \(l\), and upgrades the security level associated with the objects reachable via \(r\) as well as that of every reference \(s\) that may transitively field-alias \(r\) (\(\FieldAliasXRel s r\)).

\(\GenericRestoreObjLevels{\sHeap'}\)

upgrades the typing environment of according to that of \(\sHeap'\).

[yep]The functions specialized for the family of heap-related relations operate similarly.

[Continuing Example <ref>]

The set of variables given in the previous example are used by the operations in  <ref> to encode queries and predicates on .
We can for instance constrain so that it represents the set of all concrete heaps where r is known to be using \(\HeapInit[\fvar]{\{\cv r\}} = (\chlvl[\fvar] r = ⊥ ∧ ¬\cAliasRel[\fvar] r s ∧ ¬\cFieldAliasXRel[\fvar] r r ∧ ¬\cFieldAliasXRel[\fvar] r s)\mbox,%
\) or build the abstract transformer \(\NoHeapEffect{\cv r ← \cv s}{\fvar} = [\chlvl[\fvar]r\assign\chlvl[\fvar]s, \cAliasRel[\fvar]r s \assign \tt, \cFieldAliasXRel[\fvar] r r \assign \ff, \cFieldAliasXRel[\fvar] r s \assign \ff]\) that encodes the semantics of statement @r =<EMAIL_ADDRESS>
§ SECURE HEAP ABSTRACTION

To specify the semantics of heap operations performed by a program, we define a concrete   heap domain that maintains the value of primitive fields in addition to the precise heap-related relations.
A concrete heap domain is defined similarly to that of abstract heap domains introduced in Section <ref>, with the difference that the heap maintains the primitive fields instead of security levels.
The concrete heap domain is defined as $\ConcreteHeapDom {} = \langle\HeapDom \concrete , \Transformers \concrete  \rangle$

where \(\concrete ≝ 〈\{\AliasRelSymbol, \FieldAliasRelSymbol\}, ∅ 〉\),

the relation is an ordinary reference aliasing relation,

and is a field-aliasing relation, \(\FieldAliasRelConcrete r s f\) holds iff
the field $f$ of the object referenced by \(r\) is an alias of
\(s\).

presents the operations on the concrete heap domain.
The notation 𝑜𝑝 shows the predicate transformer that corresponds to the operation $\mathit{op}$ on a concrete heap $\mHeap \in \HeapDom \concrete$.
The functions op and op respectively specify the updates to the concrete heap-related relations and the primitive fields of the heap  by performing the heap operation $\mathit{op}$.
, and show  the set of reference fields, the default value and the undefined value, respectively.

\begin{align*}
\ConcreteHeapTransformer {op} \mHeap
\begin{array}{@{}l@{\,}l@{\,}l@{~\text{if~}}l}
\IStoreRef r {f_r} s {\mHeap} & & &  \mathit{op}= \s{r.f_r = s} \\
\ILoadRef{r} s {f_r}{\mHeap}  &&%\SQMergei  {u} & [\RefContent r \mHeap:= \RefContent {r'} \mHeap]
& 		\mathit{op}= \s{r = s.f_r}\ \\
%		  ∧ \multicolumn 4 r {\mHeap \models \FieldAliasRelConcrete s {r'} {f_r}} \\
\ICopyRef {r}{s}{\mHeap}  &\SQMergei u &
\IUpdatePrimFields {\mHeap} {op} %
%[\RefContent r \mHeap:= \RefContent s \mHeap]
& \mathit{op}= \s{r = s}  \\
\IResetRef {r = \_}{\mHeap} & \SQMergei u &
\IUpdatePrimFields {\mHeap} {op}
%\SQMergei  u & [\RefContent r \mHeap:= \newObj]
&\mathit{op}=\s{r = \cnew} \\
\IResetRef {r = \_} {\mHeap} &	\SQMergei  u &
%[\RefContent r \mHeap:= \Nil]
\IUpdatePrimFields {\mHeap} {op}
& \mathit{op}= \s{r = \Null}  \\
&& [v:= \RefContent {s}{f_p}  ]
& 		\mathit{op}= \s{v =  {s.f_p}} \\
&&		\IUpdatePrimFields {\mHeap} {op}
%[\RefContent {r}{f_p}   := v]_\mHeap
&  \mathit{op}= \s{r.f_p = v} \\
\end{array}
\right.
\end{align*}

\begin{align*}
\IResetRef{r = \_}{\mHeap} &≝
\SQMergeu_{\mathllap{ r'∈R, f \in} \RefFields}%
［\begin{array}{@{}r@{\ }l@{\ }r@{}}
\AliasRel r {r'} \assign  \ff ,
\FieldAliasRelConcrete r {r'} f \assign  \ff ,
\FieldAliasRelConcrete {r'} r f \assign  \ff
\end{array}］
\\
\ICopyRef{r}{s}{\mHeap} &≝
% \tag*{\(\displaystyle
\SQMergeu_{\mathllap{r'∈R, f \in} \RefFields}%
［\begin{array}{@{}r@{\ }l@{\ }r@{}}
\AliasRel   r {r'} \assign \AliasRel s  {r'} ,
\FieldAliasRelConcrete r {r'} f  \assign  \FieldAliasRelConcrete s {r'} f  ,
\FieldAliasRelConcrete {r'}  r  f \assign  \FieldAliasRelConcrete {r'}  s f
\end{array}］
% \)}\nonumber
\\
\ILoadRef{r} s {f_r}{\mHeap}  &≝
% \tag*{\( \displaystyle%
\SQMergeu_{\mathllap{r'∈R, f' \in} \RefFields}%
［\begin{array}{@{}r@{\ }l@{\ }r@{}}
\AliasRel r {r'}\assign  \FieldAliasRelConcrete  s {r'} {f_r} ,
\FieldAliasRelConcrete r {r'} {f'} \assign \FieldAliasRelConcrete s {s'} {f_r} \wedge \FieldAliasRelConcrete {s'} {r'} {f'} ,
\FieldAliasRelConcrete {r'} r {f} \assign  \AliasRel {r'} s
\end{array}］%
% \)}\nonumber
\\
\IStoreRef r {f_r} s {\mHeap} &≝
% \tag*{\(\displaystyle%
\SQMergeu_{% (r',s')∈\R^2
\mathllap{\FieldAliasRelConcrete {r'} {s'} {f_r} ∈} \GenericRelVars}%
［\begin{array}{@{}r@{\ }l@{}}
\FieldAliasRelConcrete {r'} {s'} {f_r} \assign & \AliasRel {r'} r \wedge \AliasRel {s'} s %\FieldAliasRelConcrete {r'} {s'} f ∨
\end{array}］%
% \)}\nonumber
\end{align*}

\begin{align*}
\IUpdatePrimFields {\mHeap} {op} &≝
\SQMergeu_{\mathllap{f_p \in} \PrimFields {s}}%
\left\{\!\!%
\begin{array}{@{}r@{\ }l@{\ }l@{}}
& [\RefContent {s}{f_p} :=\RefContent {s}{f} ]   &\quad \text{if} \quad \mathit{op}= \s{r = s} \\
& [\RefContent {s}{f_p} :=\DefVal ]   &\quad \text{if} \quad\mathit{op}= \s{r = \cnew} \\
& [\RefContent {r'}{f_p} :=v ] &\quad \text{if}  \quad\mathit{op}= \s{r.f_p = v}, \mHeap \models \AliasRel r {r'} \\
& [\RefContent {s}{f_p} :=\UndefVal ]   &\quad \text{if} \quad\mathit{op}= \s{r = \Null}
\end{array}%
\right.%
\end{align*}

Update of alias variables in a heap from the concrete heap domain.

Since we use an abstract heap domain to model and analyze information flow via heap, we should ensure that the analysis under abstract heap domains guarantees noninterference.
To this end, we first define the notion of indistinguishable heaps and then prove that two indistinguishable heaps from the concrete domain remain indistinguishable after applying a heap transformer.
Let $\GeneralH$  be a heap from an arbitrary heap domain and \(R' \subseteq R\) be a set of references.
The reference graph over \(R'\) induced by is a labeled digraph \(\RefGraph{\GeneralH}{R'} ≝ \tuple{\Nodes \GeneralH, \Edges\GeneralH}\) where $\Nodes\GeneralH = R'$ is the set of nodes, and the edges show the heap-related relations between them,
\(\Edges\GeneralH =\{ (r,\GenericRelSymb,r') ~|~ \GeneralH \models r \GenericRelSymb r', r \in R' \vee r' \in R'\} \).

Let be an abstract heap and  be a sub-graph of R containing the low-sensitive references \(\LowRefs \sHeap= \{r ~|~\sHeap \models  (\red{\hlvl[\mHeap]r}=\low)\}\).
We say two concrete heaps are indistinguishable, if heap-related relations and  primitive fields of their low-sensitive references are identical, (i) the reference graphs corresponding to their low-sensitive portions of the heaps are isomorphic, and (ii) the valuation of primitive fields of their low-sensitive references are identical.

We say
two concrete heaps
and $\mHeap'$ from ,

are indistinguishable an abstract heap , noted by \({\mHeap =_{\sHeap} \mHeap'}\),
(i)   and ' are isomorphic, denoted by \(\RefGraph{\mHeap}{\low{}} \cong \RefGraph{\mHeap'}{\low{}}\), and

\(
%\sHeap \models  (\hlvl[\mHeap]r=\low) ⇒
\forall x.~ \mHeap \models	\RefContent{r}{f_p}= x \Leftrightarrow  \mHeap' \models	\RefContent{r} {f_p}=x \), for all $r \in \LowRefs{\sHeap}$ where $f_p$ is a primitive field.

We define the concept of secure heap abstraction, which states that two indistinguishable heaps should remain indistinguishable after applying a heap operation and its corresponding transformer at the abstract heap domain level:

The concrete heap domain  is secure an abstract heap domain R, if and only if it preserves the heap indistinguishability relation, given any concrete heaps
\((\mHeap_1, \mHeap_2) ∈ \HeapDom \concrete \times \HeapDom \concrete \)
, and an abstract heap
\(\sHeap ∈ \HeapDom \hd \) \({\mHeap_1 =_{\sHeap} \mHeap_2}\), it holds that:

(a) for all pair \((\mathit{as}, \mathit{as}'% , \mathit{asgn}_{{\HH^\LL}}
) \) of reference assignment statements and their corresponding operations on abstract heaps where
\(\mathit{as} \in \{\s{r = s}, \s{r = s.f_r}, \s{r = \Null} \} \), \({\mHeap'_1 =_{\sHeap'} \mHeap'_2}\) holds where \( \mHeap'_i= {\ConcreteHeapTransformer {\mathit{as}}{ \mHeap_i}}\), $i \in \{1,2\}$, and \(\sHeap' = \NoHeapEffect{\mathit{as}'}{\sHeap}\);

(m) for all pair \((\mathit{mu}, \mathit{mu}' ) \) of mutation statements and their corresponding operations on heaps where
\(\mathit{mu} \in \{%
\s{r.f_p = e}, \s{r.f_r = s}, \s{r = \New\,c}\}\), for all \(l ∈ \LL\) where \({\hlvl[ {\sHeap}]s } \sqsubseteq l\) if \(\mathit{mu} \) is \(\s{r.f_r = s}\), and \({\plvl e} \sqsubseteq l\) if \(\mathit{mu}\) is \(\s{r.f_p = e}\), it holds that \({\mHeap'_1 =_{{\sHeap'}} \mHeap'_2}\) where \( \mHeap'_i= {\ConcreteHeapTransformer {\mathit{mu}}{ \mHeap_i}}\), $i \in \{1,2\}$, and \(\sHeap' = \OneHeapEffect{\mathit{mu}'}{l}{\sHeap}\);

The concrete heap domain R  is secure the deep abstract heap domain R according to Definition <ref>.

See Appendix <ref>.

On the relations of two heap domains: a secure heap domain w.r.t. the concrete one will be

Partial order below is only used for computing summaries. I also don't think initialisation operator is strictly required; but that latter one may still be helpful for comprehension.
Further, \(\hvar ⊑_{\mathsf H} \hvar'\) denotes a partial order that holds whenever the abstract heap , restricted to the set of references \(R' ⊆ R\) pertaining to \(\hvar'\), over-approximates a set of heap configurations, that is greater of equal than the set of heap configurations represented by \(\hvar'\): this amounts to a pairwise comparison of security levels, one must have \(\hvar ⊑_{\mathsf H} \hvar' ⇒ (∀r∈R', \hlvl[\hvar]r ⊑ \hlvl[\hvar']r)\) (and similarly for any over-approximated fact about the heap, like a may-alias relation).

§ INFERRING POLYMORPHIC INFORMATION-FLOW GUARDS

Let us now put the heap abstraction aside, and focus on our approach for computing guards and capturing implicit flows.
We start by considering the method @f@ given in  <ref>, that does not involve any reference variable.

@f@ implements a canonical pattern used to illustrate implicit flows: if its argument v is high-sensitive, then the information output on line <ref> is also high-sensitive via an implicit flow induced by the assignment guarded by the condition on line <ref>.
For this example, our requirement demands that executing the sink statement on line <ref> does not leak confidential information.
Therefore, the guard that we want to compute for @f@ is a sufficient condition that allow us to decide whether any call to the method satisfies the confidentiality requirement based on a set of program facts available whatever the calling context.
For @f@, the latter set of facts includes, for instance, the security level of the effective argument for v, or whether the call happens in a high context (if it is guarded by a condition on high-sensitive information).

[Method f.]

[Invariant \(φ_{\cv f}\) and guard f.]

\(\begin{aligned}
% φ_{\cv f} =\,&｛ℓ_4 ⟼ \pc ⊔ \cplvl l = ⊥｝%  \red{∪}\\
φ_{\cv f}(ℓ_4) ≝\,&\pc ⊔ \cplvl l = ⊥%  \red{∪}\\
% & \red{｛ℓ_i ⟼ \tt｝_{i∈\{0,1,2,3,5\}}}
\\
\SumGuard{\cv f} =\,&\pc ⊔ \cplvl v = ⊥
\end{aligned}\)

[SCFG .]

Example method with SCFG, invariant, and resulting guard.

To achieve this, we build the SCFG
that specifies the security semantics of any method in such a way that the set of all its potential initial states encodes all the possible calling contexts for the method.
For instance, when encoding @f@ the
variable v assigned to the argument v is left uninitialized (contrary to the level l of local variable l)
Another state variable
that is
left uninitialized is , as it denotes the security level of the calling context.
[yep]Next, the safety property φ expresses constraints on security levels at
states of the transition system that typically correspond to sink statements in the method.

The security constraints require that high-sensitive data should not flow to sink statements.
Eventually, a co-reachability analysis finds the set of all initial states
from which no run ever leads to a violation of
φ; a symbolic description of this set gives us the guard for the method in terms of the
variables pertaining to the calling context, like v and for<EMAIL_ADDRESS>
then associate a safety property φ that expresses constraints on security levels at states of the SCFG,
and use a co-reachability analysis to find the set of all initial states
from which no run ever leads to a violation of

Though it's still useful to recall what the invariant is; could be removed.
We graphically represent in  <ref> the SCFG
obtained for<EMAIL_ADDRESS>The associated invariant is given in  <ref>, along with the inferred guard .

§.§ Security Semantics

We use the method @m@ and declarations of classes @A@ and @B@ given in  <ref> to illustrate our approach.

a, b, i and r are state variables that respectively model the security levels of primitive or reference variables a, b, i, and r, and take their values in the security domain .

These level variables over-approximate the true security levels: that \(\cplvl i = ⊤\) indicates that the information held in i may be of highest confidentiality level; conversely, \(\cplvl i = ⊥\) indicates that i must hold low-sensitive data.
Note that a, b, and r associate levels with the variables themselves, not with the objects they might reach in the heap.
In turn, models the security level of the calling context: \(\pc = ⊥\) indicates that the call to m happens in a low context, which means that the call does not depend on a high-sensitive condition.
If on the other hand, the call happens in a high context (\(\pc = ⊤\)), then any mutation of object or execution of a sink statement may leak high-sensitive information.
On the transition from the location \(ℓ_0\) to \(ℓ_1\), r is assigned to the context level: this reflects the implicit flow of information from the execution context to r.

The remaining elements of are dedicated to a heap abstraction

that belongs to a symbolic abstract heap domain  dedicated to the representation of abstract heaps pertaining to a given set of reference variables \(R\); for @m@ we have \(R = ｛\cv a, \cv b, \cv r｝\).
The heap abstraction is a predicate defined on two sets of state variables

and .

associates a security level variable [] r with each reference \(r ∈ R\), that represents an upper bound on the security levels of any object that is reachable via \(r\).
These variables model the security typing environments for the symbolic heaps modeled by .
In , we thus have the security level variables [] a, [] b, and [] r in addition to
a, b, and r that hold security levels for the reference variables themselves (instead of for the sets of objects they may reach).  Variables from this set are also involved in expressing invariants on sink statements, as shown in  <ref>.
In turn, the set consists of Boolean variables that describe over-approximations of heap-related relations between the references in \(R\).
A typical example of a heap-related relation is the aliasing relation, that we denote with the symbol , and which is defined as an equivalence relation where \(\AliasRel r s\) holds iff \(r\) and \(s\) point to the same object.
For @m@, a symbolic abstract heap domain that over-approximates the aliasing relation shall make use of a Boolean variable [] b r to model whether b may be an alias of r
(We give more examples of heap-related relations below.)

The notations “⋅” on transition labels are predicate transformers for

; they denote sets of assignments to variables in \(\GenericHLvlVars ∪ \GenericRelVars\).
Similarly, “⋅” in the definition of \(X_0\) is a predicate on these variables.

Observe that involves a single symbolic abstract heap .
Yet, such heaps are represented by means of predicates in a propositional logic.
Therefore, any number of abstract heaps may be used in the definition of an SCFG without compromising the tractability of a (co-)reachability analysis—this, however, has an obvious impact on scalability.
In particular, our approach for analyzing implicit flows via the heap relies on the ability of the symbolic model to simultaneously represent heap abstractions for taken and non-taken program branches; we detail this aspect in Section <ref>.

We note \(\junc m {ρ}\) the junction of a CDR ρ, and this junction always exists as we assume that return statements lead to the empty sequence of statements \(surd\).
\(\inducing m {ρ}\) is the branching statement that induces ρ, and m is the CDR that is induced by .
We further note m the set of all CDRs of \(m\); we shall omit the index method \(m\) in CDR-related notations to ease readability.

Our encoding of security semantics captures implicit flows (flows induced via the program control-flow structure) by constructing SCFGs that feature two execution modes, encoded with the help of a state variable : (i) in nominal mode (\(\uVar = \ff\)), updates to security levels reflect explicit information flows, and (ii) in upgrade analysis mode (\(\uVar = \tt\)), the information flow from the high execution context to every variable updated in every possible execution path within the Control Dependence Regions (CDRs) of the current context are captured.

A CDR ρ is a non-empty set of CFG (Control-Flow Graph) nodes that gathers every instruction that is control-dependent on a given branching statement.
This use of CDRs is inspired by previous works [Denning and Denning, 1977, Barthe et al., 2007, Liu and Milanova, 2010, Lortz et al., 2014][The classical algorithm of Ball, 1993 for computing CDRs works by identifying as a junction each dominating node in the post-dominator tree of the CFG.
Such a junction $j$ is reached by every execution path that starts from any node in the set ρ of nodes that $j$ post-dominates.
Further, one can always find a unique branching node that precedes nodes in ρ and belongs to every path from the source of the CFG to any node in ρ, and ρ is therefore a CDR.].

The code in  <ref> features a single conditional branching statement on line <ref>, which induces the CDR \(ρ_1\).
The junction of \(ρ_1\) is the statement @output$_⊥$(l)@

Two execution branches are possible within \(ρ_1\): one branch executes no statement, whereas the other performs the assignment @l = 42@ on line <ref>.
This means that the execution of the latter is dependent on the condition on line <ref>.
In the SCFG , the upgrade analysis of \(ρ_1\)
starts whenever the model reaches location \(ℓ_3\), which represents the junction of \(ρ_1\), if the branching statement that induces \(ρ_1\) (encoded by \(ℓ_1\)) was subject to a high condition.

We use a state variable to record the CDR currently subject to a high-condition.

We make use of the input variable ω to

abstract away the actual branch condition in nominal mode (since our security semantics abstracts away the values of program variables).
This is for instance the case on location \(ℓ_1\) in when \(\uVar = \ff\).
The variable ω is also used to model upgrade analyses for multiple possible program paths which can be taken non-deterministically.
In , this is the case on location \(ℓ_1\) as well, when \(\uVar = \tt\).

We give in  <ref> the set of
translation rules that
specify the security semantics of a program in terms of an SCFG.

Each location of the resulting SCFG
corresponds to a semantic location, that is defined as a
pair , ψ where
corresponds to a node in its CFG,
and ψ is a behavior mode that belongs to \(｛\jsone, \jstwo｝\) (for
ominal-or-unction and ominal
ehaviors, respectively).
The junction step ψ is used in our encoding

to distinguish the nominal mode from the upgrade
analysis stage of junctions.
Essentially, a semantic location that corresponds to a statement
that is the junction of a CDR behaves as a junction when
\(ψ = \jsone\), and according to when \(ψ = \jstwo\).
Thus, statements that are not junctions never give rise to
semantic locations where \(ψ = \jstwo\).
To clarify the translation rules, we define the helper predicate
ψ in
<ref> (where
is the retraction of : gives the set of CDRs of which is the junction), that
holds iff a semantic location \(\semloc{\stms, ψ}\) represents
an actual junction.
We use l to denote the statement identified by a label l.

The rule encodes the security semantics of
We use e to denote the security level of an expression \(e\).

from upgrade analyses in the rules.
In nominal mode, l encodes the least upper-bound between \(l\) and the context level , and \(\plvl x \assignv l\) models a strong update of the security level assigned to \(x\) with l.
In upgrade analysis mode, however, l is equal to the context level (), and \(\plvl x \assignv l\) encodes a weak update of x with .
Then, a statement \(v = r.f_p\) that loads a primitive field translates into a transition that updates v with: the upper-bound between , r, and the level of any object potentially pointed to by \(r\) as maintained by the heap abstraction ([]r) when in nominal mode; the upper-bound between and v otherwise.

and encode the alternation of nominal and upgrade analyses, and do so with the help of a placeholder abstract heap \(\hvar'\) that belongs to the same abstract heap domain as , and is also represented with state variables.
According to , when a high branch is reached, the transformer ρ:

* sets the state variable used to record the CDR currently subject to a high-condition to ρ;

* updates ; and

* stores the current heap abstraction to \(\hvar'\) by copying the values of all variables [] (resp. []) to ['] (resp. [']).

The join of abstract heaps that ends upgrade analyses is performed using a bulk upgrade.
In effect, \(\HeapBulkUpgradeFrom[\hvar]{\hvar'}\):

* upgrades the security typing environment for referenced portions of the heap according to the result of the upgrade analysis in , by joining every security level from with the corresponding level in \(\hvar'\); and

* restores every heap-related relation as saved in \(\hvar'\) when entering the upgrade analysis mode.

Call encodes the security
semantics of invocation of a method $m$ based on its polymorphic information-flow summary, which is a contract that consists of:

* an information-flow guard m that specifies the invocation conditions under which the method call is secure, there is no illegal information flow in the method.  This guard is described as constraints on the security types and heap structure of the method's formal arguments;

* an effect m about its worst potential side-effects on security levels and heap structure, that is in principle a transformer describing how the heap structure and security labels may be updated by the method.

use the
guard to enforce the desired security properties upon an invocation of $m$: this boils down to ensure that Inv. (<ref>) holds for the location ℓ in which $m$ is called.

The effect is used in Call to update the typing environment and the heap model.
In detail, \(\SumGuard {m}^{r,w}\) and \(\SumEffect {m}^{r,w}\) correspond to the aforementioned guard and effect—or a combination of several summaries in case of virtual method dispatch, where guards are combined using a conjunction, and transformers are merged—, and after substitutions \(m\)'s formal arguments.
e v l denotes the substitution of security level expression \(l\) for variable \(v\) in \(e\): this is required to upgrade the context  the receiver object
(the substitution in effects is performed in every expression on the right-hand side of assignments).

For the sake of concision, we leave the computation of polymorphic effects out of the scope of this paper.  In that respect, we want to mention that this computation is achievable, even for the cases of recursion, via an extension of our security semantics, accompanied by a dedicated processing of the co-reachability analysis results.

Also note that a sound application of effects requires abstract heaps that capture object sharing relations, not just aliasing relations.

§.§ Guard Inference Procedure

We summarize the overall analysis procedure
in  <ref>, where []m denotes the specification of the security semantics of a method \(m\) as an SCFG \(S_m\) and invariant \(φ_m\) as described above.

We represent sets of states as mappings from locations to predicates on state variables, \(\B_0\) is the set of all states that violate the invariant \(φ_m\).

\(\B_0\) associates every location that corresponds to a sink statement with a predicate on security levels for program variables that violate security requirements encoded in \(φ_m\).
Then, the set of insecure states is back-propagated via a standard co-reachability analysis embodied by , finding all states from which a given set of states may be reached, and is typically solved using a fixed-point [Ramadge and Wonham, 1989, Pnueli and Rosner, 1989].

On a symbolic finite-state system like or , this computation always terminates, and is traditionally performed using the least fixed-point (\(\mathrm{lfp}\))

\begin{equation}
\B_∞ ≝ \mathrm{lfp}\ λ\B_i.\B_0 ∪ \mathrm{pre}(\B_i)\mbox,
\end{equation}

where \(\mathrm{pre}(\B)\) gives all predecessor states of .

\(\B_∞\) associates each location with a predicate that must not hold for every subsequent path in \(S_m\) to represent secure executions.
Therefore, the guard for \(m\) can be obtained by complementing \(\B_∞(ℓ_0)\) and eliminating every state variable that does not represent a proposition from \(m\)'s calling context.

This is done with the help of
\(\mathrm{cofactor}(f, g)\), which
amounts to a partial evaluation of \(f\) all variables bound in \(g\),
this gives a predicate \(f'\) that does not involve any variable fully determined by \(g\) and \((g = \tt) ⇒ (f = f')\).

[Guard inference for f]

The application of  <ref> on method @f@ first constructs the SCFG and invariant \(φ_{\cv f}\) of  <ref>.
Then, the co-reachability and partial evaluation give

\begin{align*}
\B_0 &= ｛ℓ_4 ⟼ \pc ⊔ \cplvl l ≠ ⊥｝ \red{∪ ｛ℓ_i ⟼ \ff｝_{i∈\{0,1,2,3,5\}}} \\
\B_∞ &= ｛ℓ_0 ⟼ （\ite{¬\uVar}{\pc ⊔ \cplvl v}{\pc}）≠ ⊥｝ ∪ \B_∞' \tag{\(= \Coreach{\Sf,\B_0}\)} \\
\SumGuard{\cv f} &= \pc ⊔ \cplvl v = ⊥ \tag{\(= \mathrm{cofactor}（¬\B_∞(ℓ_0), X_0）\)}\mbox.
\end{align*}

The guard f holds whenever \(\pc = ⊥\) and \(\cplvl v = ⊥\): to satisfy the confidentiality requirement, @f@ must be called in a low context (this typically means that @f@ may execute a sink statement as is the case on line <ref>).
This also states that @f@ may leak information about the effective argument for v.

tablePolymorphic guard inference for method m, for different heap domains.

2 c with \(\B_0 = \big\{ℓ_3 ⟼ \pc ⊔ \cplvl b ⊔ \chlvl b ≠ ⊥\big\} ∪ \big\{ℓ_i ⟼ \ff\big\}_{i∈\{0,1,2,4\}}\)

_1     _0 ∪     {ℓ_2 ⟼    ⊔ b ⊔ b ⊔     (b ra ⊔ a⊥)     ≠ ⊥}

_2     _1 ∪     {ℓ_1 ⟼    ⊔ b ⊔ b ⊔    (b ra ⊔ a ⊔ i⊥) ⊔

(b ai⊥)     ≠ ⊥}

_2 ∪     {ℓ_0 ⟼    ⊔ b ⊔ b ⊔    (b ai⊥)     ≠ ⊥}

⊔ b ⊔ b ⊔    (b ai⊥) = ⊥

[origin=c]90\(\mathclap{\phantom p}\)

_1     _0 ∪     {ℓ_2 ⟼    ⊔ b ⊔     b ⊔ (b ra ⊔ a⊥)     ≠ ⊥}

_2     _1 ∪     {ℓ_1 ⟼    ⊔ b ⊔ i ⊔     b ⊔ (b ra ⊔ a ⊔ i⊥)     ≠ ⊥}

_2 ∪     {ℓ_0 ⟼    ⊔ b ⊔ i ⊔     b     ≠ ⊥}

m        ⊔ b ⊔ i ⊔     b = ⊥

[origin=c]90\(\mathclap{\phantom p}\)

_1     _0 ∪     {ℓ_2 ⟼    ⊔ b ⊔ a ⊔     b ⊔ a     ≠ ⊥}

_2     _1 ∪     {ℓ_1 ⟼    ⊔ b ⊔ a ⊔ i ⊔     b ⊔ a     ≠ ⊥}

_2 ∪     {ℓ_0 ⟼    ⊔ b ⊔ a ⊔ i ⊔     b ⊔ a     ≠ ⊥}

m        ⊔ b ⊔ a ⊔ i ⊔     b ⊔ a = ⊥

width 0pt

figureSCFG for

[Guard inference for m]

The analysis
first builds the SCFG given in  <ref>, and
associates the invariant \(\pc ⊔ \cplvl b ⊔ \chlvl b = ⊥\)
location \(ℓ_3\).
This states that,
for @m@ to be secure, this statement must be executed in a low context and given a low-sensitive reference b (\(\cplvl b = ⊥\)) that must only reach low-sensitive objects (\(\chlvl b = ⊥\)).
This gives the unsafe states shown in the first row of  <ref>, where we report a trace of the co-reachability analysis and the resulting guard for each domain.

The guard obtained with the domain is the least precise of all three, as it basically describes @m@ as insecure if it is called in high context, or whenever any of its effective arguments or objects they may reach in the heap is high-sensitive.
With this domain, the statement \(\cv r.\fa = \cv a\) (location \(ℓ_2\)) may raise the security level b since \(% ｛
\cAliasRel r b% ⟼\tt
% ｝
∈\GenericRelTauto\) (as \(\TAbase {} {\cAliasRel r b} = \TAmaybe\)
On the other hand, the inference with is able to distinguish whether b and r may alias on location \(ℓ_2\), and then rules this case out thanks to the statement \(\cv r = \New~\cv B\) (location \(ℓ_0\)).
However, the guard does not hold whenever \(\cplvl i ≠ ⊥\), as the domain cannot distinguish whether \(\cv b.\fa\) aliases \(\cv a\) or not: therefore, the statement \(\cv a.\fint = \cv i\) (location \(ℓ_1\)) always raises the level b to that of \(\pc ⊔ \cplvl i\).

At last, the domain distinguishes whether \(\cv b.\fa\) aliases \(\cv a\) or not, and the guard indicates that @m@ may not be secure if i is high-sensitive and a and b relate to each other via \(\cv b.\fa\).

which describes every state of the model that violates the security requirement (the invariant).
The analysis then proceeds with
the computation of all states \(\B_∞\) that are co-reachable to \(\B_0\), the states form which there exists a path in  that reach \(\B_0\).

Like \(\B_0\), \(\B_∞\) associates every location in with a predicate that describes unsafe states.
We can eventually obtain the guard for @m@ that only relates to its calling context (only involving state variables pertaining to the calling context) via a partial evaluation generalized cofactor as on line <ref> in  <ref>.

§ SOUNDNESS

We prove that any program guarded with a security guard inferred by our method guarantees termination-insensitive noninterference [Sabelfeld and Myers, 2003].
This notion states that, for any initial states $\qstate$ and $\qstate'$ whose secret parts may only differ, the observation sequences of the program running from the states $\qstate$ and $\qstate'$ will either be the same, or one is a prefix of the other.
The reason for the latter case is that this notion is a termination-insensitive property.

Let \(\S \) denote the (symbolic) full semantics of a program,
and $\FSM\S=\FSMdef$ be an automaton that describes its concrete

where is the set of states, $\mathcal{I}$ is the set of inputs,

$\smTrans \subseteq \smStates \times \smStates$ is the set of transitions and $\smStates_0$ is the set of initial states.
A program state \(\qstate % \in \smStates
\) is defined as
\(\mframeX {{\VarsTypes}} {ℓ} \V {\X} \mHeapVal\)

is the current location,

is the
valuation for every one of the

primitive program variables $\PrimVars$,
\(\VarsTypes: \PrimVars \cup R
→ \LL\) is the security typing environment for the primitive variables $\PrimVars$ and references $R$,
\(\X
%∈ \Val{X}
\)
is the current valuation of the state variables of the security semantics except the location and the typing environment for the references.
We use the notation
$\X_{\sHeap} {}$ to show
's heap abstraction ,
to denote its security typing environment.
Furthermore, is the valuation of the concrete heap's variables.

Let $\qstate \xrightarrow{\eta}_* \qstate'$ be an execution of full semantics  with a non-zero length (the reflexive and transitive closure of the concrete transition relation $\smTrans$) from the state $\qstate$ to the state $\qstate'$, where $\eta \in \{o,\bot\}$.
This execution either ends by executing a statement that outputs on a channel ($\eta=o$)
or makes no observation ($\eta = \bot$).
We denote an execution that never reaches an observation point by $\qstate \xrightarrow{\bot}_* $.
We define noninterference based on a low-equivalence relation, that states that the public parts of the two states $\qstate_1$ and $\qstate_2$ are indistinguishable.

We say  two valuations $\V_1 ∈ \Val \PrimVars$ and $\V_2 ∈ \Val \PrimVars$ are low-equivalent the typing environment \(\VarsTypes: \PrimVars \cup R→ \LL\),
denoted by \(\V_1 =_{\VarsTypes} \V_2\),
iff $\V_1(v) = \V_2(v)$ for all $v ∈ \PrimVars$ where \(\VarsTypes(v)=\low\).

We say two states \( \qstate_i=\mframeX{{\VarsTypes_i}}{ℓ}{\V_i}{\X_i}{\mHeapVal_i},  i\in\{1,2\}\)

are compatible,
denoted by \(\qstate_1 \approx \qstate_2 \), iff  (i) \( {\VarsTypes_1}=\VarsTypes_2\),

(ii) ${\sHeapValLevs {\X_1} \sHeap}={\sHeapValLevs {\X_2} \sHeap}$,
(iii) \(\V_1 =_{\VarsTypes_1} \V_2\),
and (iv) \({\mHeapVal_1 =_{{\X_1}_{\sHeap}} \mHeapVal_2}\).
They are called
low-bisimilar, denoted by $\qstate_1 \lowbisim \qstate_2$, iff \(\qstate_1 \approx \qstate_2\), and  if $\qstate_1\xrightarrow{o}_* \qstate'_1$,
then either (a) there exists $\qstate'_2$ such that $\qstate_2 \xrightarrow{o}_* \qstate'_2$
and $\qstate_1' \lowbisim \qstate'_2$,
or (b) $\qstate_2 \xrightarrow{\bot}_* $,
and vice versa.

For any method $m$ guarded by a security guard m, and any initial states \( \qstate_1\) and  \( \qstate_2\) where	\(\qstate_1\approx \qstate_2\) and

$\qstate_i\models \SumGuard m $,
$i \in \{1,2\}$, it holds $\qstate_1 \lowbisim\qstate_2$.

To prove this theorem, we show that there exists a witnessing bisimulation relation
for $\qstate_1 \lowbisim \qstate_2$. See Appendix <ref>.

§ IMPLEMENTATION AND EVALUATION

To empirically validate our approach, we assess the respective performances of our three heap domains on actual code, both in terms of precision and scalability.

§.§ Implementation Details

We have first implemented a tool that relies on  [Vallée-Rai et al., 2010] to obtain the code of a program, and translates it into our input language.
is an intermediate language to represent byte-code at a higher level.
The semantics of its instructions and reference manipulations correspond to that of the .
One statement roughly translates into one statement of our input language.

We have then implemented the guard inference algorithm in a prototype tool called [Available as a software artifact [Berthier and Khakpour, 2022], with user documentation and source code at <http://nberth.space/symmaries>.], that features multiple instantiations of our heap domains.
's pre-analysis relies on a naive analysis of the class hierarchy to construct a graph that allows us to compute facts about heap-related relations (function ).

This tool relies on  [Berthier and Marchand, 2014] to solve the co-reachability problems.

uses (Multi-terminal) Binary Decision Diagrams—(MT)BDDs— [Bryant, 1986, Billon, 1987] to represent symbolic expressions and compute the underlying fixed-points.

Can be removed now?

§.§.§ Interprocedural Analysis

Simple code often involves several methods, and our main objective for the evaluations consists in assessing the relative performances of applying our approach on actual code, using each heap domain.
Furthermore, a proper handling of precision benchmarks additionally requires the analysis to capture information-flows across method calls.
Therefore, implements an inter-procedural variant of the analysis formalized above.
Informally, the security semantics of method calls is encoded as follows:
First, reuses the guard inferred for each called method (after some renaming of arguments) to associate an invariant with semantic locations that correspond to their potential call sites.
Second, to account for the effects of callees on the heap and returned values, automatically generates predicate transformers based on signatures of called methods (the types of formal arguments).
Such transformers encode some predefined behaviors, where every portion of heap reachable via a reference argument may be mutated during the execution of the method, a high-sensitive value may be returned, etc.

To deal with

guards and transformers that encode the semantics of library methods, we rely on

stubs, given to , that describe the effects of these methods at a high level.
We manually defined the security semantics of methods from the standard and Android libraries (about 1200 methods in total) in this way.

§.§ Precision & Recall

We have employed the benchmark suite [Hamann et al., 2018] to
assess the precision of our different heap domains and compare our results to
[Ahrendt et al., 2005],
[Lortz et al., 2014], and
[Hammer and Snelting, 2009].

The precision refers to a proportion
of test cases that are correctly classified.
The recall is the fraction of true positive and false negative test cases that are categorized correctly.

provides 232 test cases that showcase various information-flow vulnerabilities in programs, with various forms of explicit

and implicit information leaks.

[yep]extends SecuriBench Micro <cit.>, that is a benchmark suite for security analyzes of web applications; it provides 152 samples derived from the original 122 samples of SecuriBench Micro.
also features all 119 samples from DroidBench <cit.>, that is a benchmark suite for evaluating taint-analysis tools that target the Android platform.

We report in  <ref> the precision results that we obtain for different abstract heap domains for the various categories of leaks and language features that
We have checked 164 out of 232 test cases supported by our sub-language: the excluded cases involve reflection, static class initializers, exceptions and method calls (11, 10, 9, and 39 samples respectively—we have excluded all cases in the latter category as they check the ability of the analysis to handle information-flows across method calls,

while we
left the problem of computing method  effects aside).
Note that a test case may belong to multiple categories.

[]Precision Results

Category           #Smpls
explicit-flows       143       80.4         79.7         78.3     70.6         77.6           72.7

implicit-flows        21       71.4     71.4     71.4     57.1         57.1           61.7

simple                51           72.5         72.5         72.5     64.7     76.4           68.6

high-cond.            10       80       80       80       60           60             60

arrays                26           73           73           69.2     65.3     76.9           69.2

library               69       88.4     88.4         86.9     76.8         76.7           79.7

aliasing              7        71.4     71.4         57.1     57.1         42.8           42.8
average                        79.2         78.6         77.4     68.9         75             71

The #Smpls column shows the number of included samples for each category
; other figures are percentages.

Since our approach is sound, we obtain 100% recall, we correctly detect every insecure flow.

Regarding precision, our experiments show that all the domains have close precision: the domain offers the highest precision of 79.2% and  offers the lowest precision of 77.4%.
The false positives (the secure test cases that were restrictively classified as insecure) mainly occur because our domains are field-insensitive, value-insensitive, do not distinguish elements in some collections of data, or due to the over-approximations in heap-related relations.

The results for the aliasing category are rather similar; 3 test cases in this category are insecure that are classified correctly by all three domains, as our analysis is sound. Two of the remaining 4 secure test cases are classified as insecure in all domains due to value- and field-insensitivity.

On average, the domain offers the best precision in five categories. It
slightly underperforms the state-of-the-art for simple and arrays test cases only, notably due to value- and field-insensitivity.
In some categories, the improvement is noticeable, it
improves the best precision of the aliasing category offered by
the existing tools by 14.3%, improves the library category by
8.7% and enhances the implicit-flows category by 9.5%. We
attribute these substantial results in part to our precise handling of implicit flows across method calls (unlike which forbids method calls in high-contexts for instance), and
in part to our heap abstract domain, that is able to precisely
track some intricate aliasing relations.
That most of our domains obtain similar precision results on the aliasing category may indicate that these test cases are rather uniform in the facts about aliasing that need to be discovered to detect secure cases.

Our findings show that while different domains had close precision results, they offer different computational complexity though.
IFSpec only partially covers the set of IFC problems one can encounter in practice; we therefore refrain from generalizing our results. Yet, IFSpec is the most extensive benchmark available for IFC that we know of.

Density plots showing the distributions of analyzed ABM methods both the number of reference variables (horizontal axes) and the analysis time (vertical axes).  Note the shared log scales, including on the color-bars.

Scalability Evaluation

We have conducted experiments on real-life web applications to compare different heap abstract domains in terms of scalability.
To accommodate computationally intensive analyses, we

interrupt any analysis after 5 minutes or if it uses more than 4GB of
We have used applications from the ABM benchmark [Do et al., 2016],
a collection of 139 open-source projects that is dedicated to the
evaluation of static analyzers for applications.
Its content is deemed representative of real-world software, and has
already been used for evaluating static taint analysis and dead code
elimination approaches [Do et al., 2016].
From this collection, we extracted the code from 60
applications with sizes ranging from 133 to 25K lines of .
This provided us with a total of
22512 analyzable methods.
Overall, the domain led to 146 analyses being interrupted due
to the timeouts or memory limitations (3 for ,
0 for ).

We plot in  <ref>, for each domain, the distributions of successful analyses the number of reference variables and analysis time.
As expected, analysis times grow with the amount of references, and by factors that depend on the heap-related relations captured flow-sensitively by the domains,

is more expensive compared to and .

Further, many methods have fewer than 10 reference variables, and as a result most analysis times do not exceed 0.1s for every domain.
Those figures empirically support the applicability of our approach on real-life applications.

Plots showing for each domain, the proportions of unsatisfiable (top) and tautological (bottom) guards number of reference variables.

Note that an ideal study on the scalability of different heap domains would compare the domains under different analysis techniques, provided by different tools.
This, however, requires the support of the existing tools for modeling different heap domains.
To the best of our knowledge, there was no such tool, as each implementation is typically tied with its own heap model, if any at all.
Otherwise, extending the tools to support different heap domains is virtually infeasible since most existing tools rely on store-based models.
To further compare the respective precision of each domain, we also report in  <ref> the ratios of unsatisfiable and tautological guards obtained for each domain.
We observe that the precision of all domains seems similar when the number of reference variables is low, and diverges with growing numbers of references.

appears to be more permissive than and for methods with many references.
However, that

did not produce unsatisfiable guards for methods with more than 29 references indicates that many analyses of such methods were interrupted.

§ RELATED WORKS

Static analysis approaches to ensure noninterference have been studied
extensively in the community
The vast majority of suggested IFC solutions concentrates on
type-systems <cit.>, and

various tools that target realistic programming languages have been developed for verifying such properties.
Prominent examples include
JFlow JIF [Sabelfeld and Myers, 2003], FlowCaml [Pottier and Simonet, 2003],  [Lortz et al., 2014], and  <cit.>.
, the aforementioned approaches often lack

precision in practice ( [Lortz et al., 2014]), or require
user intervention, such
as the specification of loop invariants
( [Sabelfeld and Myers, 2003]).

Another line of research trades efficiency for soundness and/or precision,
by exploiting more generic
techniques like interprocedural dataflow analysis <cit.> or program slicing <cit.>.

JOANA <cit.>, DroidSafe [Gordon et al., 2015] and FlowDroid [Arzt et al., 2014] are prominent frameworks in this category.

solutions are dedicated to web
applications <cit.> or Android apps [Li et al., 2017], although
most of them do not handle implicit flows or lack soundness ( [Hammer and Snelting, 2009, Gordon et al., 2015, Arzt et al., 2014]).
Tools that provide sound results via other forms of global program analyses include
HornDroid <cit.>, which
does not capture implicit flows.

In contrast to the above methods, our approach is proven sound, captures implicit flows (via heap), and our experiments show that it improves the state-of-the-art precision.

Further, the above approaches

often rely on a simple store-based representation of the heap specified as a mapping from
references (or abstract locations) to
heap locations [Amtoft et al., 2006, Barthe et al., 2007, Lortz et al., 2014],
or do not rely on a flow-sensitive heap abstraction [Lortz et al., 2014].

By contrast, we use a store-less representation, where the structure of the heap is specified using a parameterizable family of (possibly over-approximated) relations.
This offers different levels of over-approximation and complexity, enabling the user to easily trade-off performance and scalability.

Static Analysis approaches for information flow control are often logic-based, or type system-based.
A flow-sensitive information flow analysis for object-oriented programs via a Hoare-style logic has been presented in [Amtoft et al., 2006]. The logic employs region assertions to describe possible aliasing, and independence assertions to describe indistinguishablity to formalize non-interference.
A flow-insensitive type system for reasoning about a Java-like language is proposed in <cit.>, that requires manually annotating all fields, method parameters and method signatures with security types.
Jif <cit.> is a well-known tool that extends Java with security types to support information flow control in Java applications.
While Jif is helpful to develop secure programs, it may require significant effort for annotating the programs.
Joana <cit.>, is a static analysis tool for information flow control in Java applications that uses program dependence graphs (PDGs) to represent the programs, and employs program slicing to check whether a source may influence a sink.
[Lortz et al., 2014] is a sound solution that targets a realistic object-oriented low-level language.

As shown by our experiments, our approach outperforms the existing work in terms of precision. Even the least precise instantiation of our work, offers a better precision. Further, we employ a synthesis-based approach to synthesize a guard rather than using a verification-based.

Few works have addressed the problem of capturing implicit flows while exploiting flow-sensitive heap abstractions [Khakpour, 2021, Khakpour and Skandylas, 2018, Zanioli et al., 2012].
Khakpour, 2021 synthesizes sound security monitors that enforce IFC by using a symbolic discrete control algorithm.
This work
operates intraprocedurally on high-level programs and
uses an field-sensitive heap abstraction that does not scale well.
Zanioli et al., 2012 advance an abstract-interpretation-based analysis, where the construction of the heap abstraction is delegated to a separate analysis.
Their analysis can operate on a flow-sensitive abstraction as produced by a TVLA-based shape analysis [Sagiv et al., 2002], yet it can only be applied to small, high-level programs.

Other forms of
symbolic heap abstractions have already been used in static program analysis.
Separation logic [Reynolds, 2002] models a heap
as a formula that comprises atomic predicates combined using the separation operator.

While we use a store-less representation of the heap
expressed using a proposition, symbolic heaps in separation logic are store-based, more expressive, and consequently are more complex for verification.

heap abstractions are also polymorphic

and enable us to operate on each method of the program in isolation.
This is to be contrasted with traditional data-flow analysis [Reps et al., 1995], where flow functions must be distributive and expressed on finite domains (as typically provided by store-based abstractions).

Supervisory control has been increasingly applied in various domains, such as industrial automation <cit.>, or the control of computing systems, for
deadlock avoidance
Contrary to the works on IFC that follow a pragmatic, programming-language approach to define security properties , these notions in the DCS community are defined in terms of event traces (input/output sequences) and studied using Petri Nets and Timed or classical Automata formalisms.
<cit.> give a very good overview of the various approaches for defining non-interference in this context.

In the DES community, however, recent works address opacity properties, a notion that encompasses other security-related properties such as anonymity <cit.> in addition to non-interference: a system is opaque if, for any secret behavior (execution trace), there exists at least one non-secret behavior (observable execution trace) that looks indistinguishable to the intruder.
This definition is more general as it is agnostic to the observational capabilities of attackers .
Several works address the problem of opacity enforcement, although often with varying definitions of this property <cit.>.

§ CONCLUSION

We have introduced a generic abstract heap domain for modeling heaps and information flow via heap for low-level object-oriented programs, and instantiated it with different families of relations. Our experiments
showed that our instantiated heap models

improve the state-of-the-art precision, and that the precision has an inverse relationship with scalability.

We are currently investigating the computation of

method summaries in order to obtain a fully modular interprocedural IFC analysis.

Indeed, our approach for symbolically abstracting the heap and encoding the security semantics effectively supports the design of sound and modular (bottom-up) interprocedural IFC analyses, where the analysis of a method provides a polymorphic artifact.
Such an artifact is directly re-usable at any call site of the method (modulo renaming of formal arguments), thereby limiting the needs for re-analyzing methods to the cases of (mutual) recursion.
Such a modular analysis is scalable since it focuses on one method at a time.

can be improved by implementing a more advanced analysis to reduce the amount of symbolic variables involved

to represent the heap, thereby improving scalability.
Further, the instantiated heap domains are field-insensitive, and a natural
extension is introducing support for field-sensitive analyses.

See <cit.> “Polymorphic Predicate Abstraction”, for the use of the term “polymorphic” to denote the symbolic variables that represent the unknown context.
Mizuno and Schmidt, 1992 also seem to be modular via symbolic variables.

One family of static approaches for IFC mostly concentrates on

type-systems [Pottier and Simonet, 2003, Sabelfeld and Myers, 2003, Barthe et al., 2007, Hedin and Sabelfeld, 2012].

Another line of research focuses on

program slicing <cit.>
, where a large graph (often called a Program Dependence Graph—PDG) is derived from the entire application, and then used to answer queries about information flows.
<cit.>, DroidSafe [Gordon et al., 2015], FlowDroid [Arzt et al., 2014], and  [Johnson et al., 2015] are prominent frameworks in this category.
“PIDGIN PDGs are context sensitive, object sensitive, and field sensitive. They are flow sensitive for local variables and flow-insensitive for heap locations.”
XXX:  [Lortz et al., 2014] (individually types each field declared in the app; field-types are fixed for the whole app; object- and flow-insensitive heap abstraction. What about  [Ahrendt et al., 2005, Darvas et al., 2005] (needs manual inputs)?
All the aforementioned approaches have one key ingredient in common: they “consume points-to information” provided by some other analysis.

About traditional models of the heap: Even points-to analyses “rarely” path- or flow-sensitive according to <cit.> (yet they provide a flow-insensitive points-to analysis).

<cit.> is a whole-program analysis, but is relevant in that they over-approximate flow-sensitive variable reachability information via abstract-interpretation; implemented in juliasoft, with many client analyses whose precision and efficiency is then improved ().  Abstract domain is simply a set of variable pairs, an extensional representation of the variable reachability relation.  Can also reuse pre-established facts about possible sharing and definite aliasing.  Not strictly related to security aspects.

The only work we have found that does consider implicit flows with a flow-sensitive heap abstraction was developed by Zanioli et al., 2012

; it however only operates intra-procedurally and on high-level structured programs.
<cit.>: abstract interpretation approach with encoding of all variable dependencies via propositional formula and fixpoint over Pos domain for each statement — specific to two-level lattice; re-uses TVLA-based heap abstract domain to dwal with ; implicit flows as well; structured programs only.

What about optimization by limiting alias info to relevant context (see <cit.>)?
See <cit.> as well, similar to RCI but with summary conditions represented as access paths instead (Context insensitive modular points-to analysis for C with function pointers).

See <cit.>, Section 7, for a link to a seminal work on the Symbolic Relational Separate Analysis method (except that we use a backwards analysis to simultaneously compute the pre-condition and post-conditions).

§.§.§ Acknowledgements

The first author was supported by the UK Engineering and Physical Sciences Research Council (EPSRC) through grant EP/M027287/1, and the second author was supported by the Swedish Knowledge Foundation (KKs) via the grant 20160186.

[Goguen and Meseguer, 1982]
J. A. Goguen and J. Meseguer.
Security Policies and Security Models.
In 1982 IEEE Symposium on Security and Privacy, pages 11–20,
Los Alamitos, CA, USA, April 1982. IEEE Computer Society.

[Pottier and Simonet, 2003]
François Pottier and Vincent Simonet.
Information Flow Inference for ML.
ACM Trans. Program. Lang. Syst., 250 (1):0
117–158, January 2003.
ISSN 0164-0925.
URL <http://doi.acm.org/10.1145/596980.596983>.

[Sabelfeld and Myers, 2003]
A. Sabelfeld and A. C. Myers.
Language-based information-flow security.
IEEE Journal on Selected Areas in Communications, 210
(1):0 5–19, January 2003.
ISSN 0733-8716.

[Barthe et al., 2007]
Gilles Barthe, David Pichardie, and Tamara Rezk.
A Certified Lightweight Non-interference Java Bytecode Verifier.
In Proceedings of the 16th European Symposium on Programming,
ESOP'07, pages 125–140, Berlin, Heidelberg, 2007. Springer-Verlag.
ISBN 978-3-540-71314-2.
URL <http://dl.acm.org/citation.cfm?id=1762174.1762189>.

[Liu and Milanova, 2010]
Yin Liu and Ana Milanova.
Static information flow analysis with handling of implicit flows and
a study on effects of implicit flows vs explicit flows.
In Proceedings of the 2010 14th European Conference on Software
Maintenance and Reengineering, CSMR '10, pages 146–155, USA, 2010. IEEE
Computer Society.
ISBN 9780769543215.
URL <https://doi.org/10.1109/CSMR.2010.26>.

[Hedin and Sabelfeld, 2012]
Daniel Hedin and Andrei Sabelfeld.
Information-Flow Security for a Core of JavaScript.
In Proceedings of the 2012 IEEE 25th Computer Security
Foundations Symposium, CSF '12, pages 3–18, Washington, DC, USA, 2012. IEEE
Computer Society.
ISBN 978-0-7695-4718-3.
URL <http://dx.doi.org/10.1109/CSF.2012.19>.

[Barthe et al., 2011]
Gilles Barthe, Pedro R D'argenio, and Tamara Rezk.
Secure information flow by self-composition.
Mathematical Structures in Computer Science, 210
(6):0 1207–1252, 2011a.

[Terauchi and Aiken, 2005]
Tachio Terauchi and Alex Aiken.
Secure Information Flow As a Safety Problem.
In Proceedings of the 12th International Conference on Static
Analysis, SAS'05, pages 352–367, Berlin, Heidelberg, 2005. Springer-Verlag.
ISBN 3-540-28584-9, 978-3-540-28584-7.
URL <http://dx.doi.org/10.1007/11547662_24>.

[Barthe et al., 2011]
Gilles Barthe, Juan Manuel Crespo, and César Kunz.
Relational verification using product programs.
In Proceedings of the 17th International Conference on Formal
Methods, FM'11, pages 200–214, Berlin, Heidelberg, 2011b.
ISBN 9783642214363.

[Darvas et al., 2005]
Ádám Darvas, Reiner Hähnle, and David Sands.
A theorem proving approach to analysis of secure information flow.
In Dieter Hutter and Markus Ullmann, editors, Security in
Pervasive Computing, pages 193–209, Berlin, Heidelberg, 2005. Springer
Berlin Heidelberg.
ISBN 978-3-540-32004-3.

[Mizuno and Schmidt, 1992]
Masaaki Mizuno and David Schmidt.
A security flow control algorithm and its denotational semantics
correctness proof.
Form. Asp. Comput., 40 (1):0 727–754,
November 1992.
URL <https://doi.org/10.1007/BF03180570>.

[Zanotti, 2002]
Mirko Zanotti.
Security typings by abstract interpretation.
In Proceedings of the 9th International Symposium on Static
Analysis, SAS '02, pages 360–375, Berlin, Heidelberg, 2002.
ISBN 3540442359.

[Giacobazzi and Mastroeni, 2004]
Roberto Giacobazzi and Isabella Mastroeni.
Abstract non-interference: Parameterizing non-interference by
abstract interpretation.
In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL '04, pages 186–197, New York, NY,
USA, 2004. Association for Computing Machinery.
ISBN 158113729X.
URL <https://doi.org/10.1145/964001.964017>.

[Zanioli et al., 2012]
Matteo Zanioli, Pietro Ferrara, and Agostino Cortesi.
Sails: Static analysis of information leakage with sample.
In Proceedings of the 27th Annual ACM Symposium on Applied
Computing, SAC '12, pages 1308–1313, New York, NY, USA, 2012. Association
for Computing Machinery.
ISBN 9781450308571.
URL <https://doi.org/10.1145/2245276.2231983>.

[Kanvar and Khedker, 2016]
Vini Kanvar and Uday P. Khedker.
Heap Abstractions for Static Analysis.
ACM Comput. Surv., 490 (2):0 29:1–29:47, June
ISSN 0360-0300.
URL <http://doi.acm.org/10.1145/2931098>.

[Vallée-Rai et al., 2010]
Raja Vallée-Rai, Phong Co, Etienne Gagnon, Laurie Hendren, Patrick Lam, and
Vijay Sundaresan.
Soot: A Java bytecode optimization framework.
In CASCON First Decade High Impact Papers, pages 214–224.

[Hammer and Snelting, 2009]
Christian Hammer and Gregor Snelting.
Flow-sensitive, Context-sensitive, and Object-sensitive Information
Flow Control Based on Program Dependence Graphs.
Int. J. Inf. Secur., 80 (6):0 399–422,
October 2009.
ISSN 1615-5262.
URL <http://dx.doi.org/10.1007/s10207-009-0086-1>.

[Gordon et al., 2015]
Michael I. Gordon, Deokhwan Kim, Jeff H. Perkins, Limei Gilham, Nguyen Nguyen,
and Martin C. Rinard.
Information Flow Analysis of Android Applications in DroidSafe.
In 22nd Annual Network and Distributed System Security
Symposium, NDSS 2015, San Diego, California, USA, February 8-11, 2015. The
Internet Society, 2015.

[Arzt et al., 2014]
Steven Arzt, Siegfried Rasthofer, Christian Fritz, Eric Bodden, Alexandre
Bartel, Jacques Klein, Yves Le Traon, Damien Octeau, and Patrick McDaniel.
FlowDroid: Precise Context, Flow, Field, Object-sensitive and
Lifecycle-aware Taint Analysis for Android Apps.
In Proceedings of the 35th ACM SIGPLAN Conference on
Programming Language Design and Implementation, PLDI '14, pages 259–269,
New York, NY, USA, 2014. ACM.
ISBN 978-1-4503-2784-8.
URL <http://doi.acm.org/10.1145/2594291.2594299>.

[Johnson et al., 2015]
Andrew Johnson, Lucas Waye, Scott Moore, and Stephen Chong.
Exploring and enforcing security guarantees via program dependence
In Proceedings of the 36th ACM SIGPLAN Conference on
Programming Language Design and Implementation, PLDI '15, pages 291–302,
New York, NY, USA, 2015. Association for Computing Machinery.
ISBN 9781450334686.
URL <https://doi.org/10.1145/2737924.2737957>.

[Lortz et al., 2014]
Steffen Lortz, Heiko Mantel, Artem Starostin, Timo Bähr, David Schneider,
and Alexandra Weber.
Cassandra: Towards a Certifying App Store for Android.
In Proceedings of the 4th ACM Workshop on Security and Privacy
in Smartphones & Mobile Devices, SPSM '14, pages 93–104, New York, NY,
USA, 2014. ACM.
ISBN 9781450331555.
URL <https://doi.org/10.1145/2666620.2666631>.

[Boudol, 2009]
Gérard Boudol.
Secure information flow as a safety property.
In Pierpaolo Degano, Joshua Guttman, and Fabio Martinelli, editors,
Formal Aspects in Security and Trust, pages 20–34, Berlin,
Heidelberg, 2009. Springer Berlin Heidelberg.
ISBN 978-3-642-01465-9.

[Ramadge and Wonham, 1989]
Peter J. G. Ramadge and W. Murray Wonham.
The Control of Discrete Event Systems.
Proceedings of the IEEE; Special issue on Dynamics of Discrete
Event Systems, 770 (1):0 81–98, 1989.

[Pnueli and Rosner, 1989]
Amir Pnueli and Roni Rosner.
On the Synthesis of a Reactive Module.
In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL '89, pages 179–190, New York, NY,
USA, 1989. Association for Computing Machinery.
ISBN 0897912942.
URL <https://doi.org/10.1145/75277.75293>.

[Hamann et al., 2018]
Tobias Hamann, Mihai Herda, Heiko Mantel, Martin Mohr, David Schneider, and
Markus Tasch.
A uniform information-flow security benchmark suite for source code
and bytecode.
In Nils Gruschka, editor, Secure IT Systems, pages 437–453,
Cham, 2018. Springer International Publishing.
ISBN 978-3-030-03638-6.

[Do et al., 2016]
Lisa Nguyen Quang Do, Michael Eichberg, and Eric Bodden.
Toward an Automated Benchmark Management System.
In Proceedings of the 5th ACM SIGPLAN International Workshop on
State Of the Art in Program Analysis, SOAP 2016, pages 13–17, New York, NY,
USA, 2016. Association for Computing Machinery.
ISBN 9781450343855.
URL <https://doi.org/10.1145/2931021.2931023>.

[Denning and Denning, 1977]
Dorothy E. Denning and Peter J. Denning.
Certification of programs for secure information flow.
Commun. ACM, 200 (7):0 504–513, July 1977.
ISSN 0001-0782.
URL <https://doi.org/10.1145/359636.359712>.

[Ball, 1993]
Thomas Ball.
What's in a Region? Or Computing Control Dependence Regions in
near-Linear Time for Reducible Control Flow.
ACM Lett. Program. Lang. Syst., 20 (1–4):0
1–16, March 1993.
ISSN 1057-4514.
URL <https://doi.org/10.1145/176454.176456>.

[Berthier and Khakpour, 2022]
Nicolas Berthier and Narges Khakpour.
Artifact for Paper (Symbolic Abstract Heaps for Polymorphic
Information-flow Guard Inference), September 2022.
URL <https://doi.org/10.5281/zenodo.7103855>.

[Berthier and Marchand, 2014]
Nicolas Berthier and Hervé Marchand.
Discrete Controller Synthesis for Infinite State Systems with
In 12th Int. Workshop on Discrete Event Systems, WODES '14,
pages 46–53. IFAC, May 2014.
ISBN 978-3-902823-61-8.

[Bryant, 1986]
Randal E. Bryant.
Graph-based algorithms for boolean function manipulation.
IEEE Trans. Comput., 350 (8):0 677–691,
August 1986.
ISSN 0018-9340.
URL <https://doi.org/10.1109/TC.1986.1676819>.

[Billon, 1987]
J. P. Billon.
Perfect normal forms for discrete programs.
Technical report, Bull, 1987.

[Ahrendt et al., 2005]
Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese,
Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen
Schlager, and Peter H. Schmitt.
The key tool.
Softw. Syst. Model., 40 (1):0 32–54, February
ISSN 1619-1366.
URL <https://doi.org/10.1007/s10270-004-0058-x>.

[Reps et al., 1995]
Thomas Reps, Susan Horwitz, and Mooly Sagiv.
Precise Interprocedural Dataflow Analysis via Graph Reachability.
In Proceedings of the 22Nd ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL '95, pages 49–61, New York, NY,
USA, 1995. ACM.
ISBN 0-89791-692-1.
URL <http://doi.acm.org/10.1145/199448.199462>.

[Kam and Ullman, 1977]
John B. Kam and Jeffrey D. Ullman.
Monotone Data Flow Analysis Frameworks.
Acta Inf., 70 (3):0 305–317, September 1977.
ISSN 0001-5903.
URL <http://dx.doi.org/10.1007/BF00290339>.

[Hedin et al., 2014]
Daniel Hedin, Arnar Birgisson, Luciano Bello, and Andrei Sabelfeld.
JSFlow: Tracking information flow in JavaScript and its APIs.
In Proceedings of the 29th Annual ACM Symposium on Applied
Computing, pages 1663–1671. ACM, 2014.

[Li et al., 2017]
Li Li, Tegawendé F Bissyandé, Mike Papadakis, Siegfried Rasthofer,
Alexandre Bartel, Damien Octeau, Jacques Klein, and Le Traon.
Static analysis of android apps: A systematic literature review.
Information and Software Technology, 88:0 67–95,

[Calzavara et al., 2016]
S. Calzavara, I. Grishchenko, and M. Maffei.
HornDroid: Practical and Sound Static Analysis of Android
Applications by SMT Solving.
In 2016 IEEE European Symposium on Security and Privacy
(EuroS&P), pages 47–62, March 2016.

[Calzavara et al., 2017]
S. Calzavara, I. Grishchenko, A. Koutsos, and M. Maffei.
A Sound Flow-Sensitive Heap Abstraction for the Static Analysis of
Android Applications.
In 30th Computer Security Foundations Symposium, CSF'17, pages
22–36. IEEE, August 2017.

[Amtoft et al., 2006]
Torben Amtoft, Sruthi Bandhakavi, and Anindya Banerjee.
A logic for information flow in object-oriented programs.
In J. Gregory Morrisett and Simon L. Peyton Jones, editors,
Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages, POPL 2006, Charleston, South Carolina, USA,
January 11-13, 2006, pages 91–102. ACM, 2006.
URL <https://doi.org/10.1145/1111037.1111046>.

[Khakpour, 2021]
Narges Khakpour.
A field-sensitive security monitor for object-oriented programs.
Comput. Secur., 108:0 102349, 2021.
URL <https://doi.org/10.1016/j.cose.2021.102349>.

[Khakpour and Skandylas, 2018]
Narges Khakpour and Charilaos Skandylas.
Synthesis of a Permissive Security Monitor.
In European Symposium on Research in Computer Security, pages
48–65. Springer, 2018.

[Sagiv et al., 2002]
Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm.
Parametric shape analysis via 3-valued logic.
ACM Trans. Program. Lang. Syst., 240 (3):0
217–298, May 2002.
ISSN 0164-0925.
URL <https://doi.org/10.1145/514188.514190>.

[Reynolds, 2002]
John C. Reynolds.
Separation Logic: A Logic for Shared Mutable Data Structures.
In Proceedings of the 17th Annual IEEE Symposium on Logic in
Computer Science, LICS '02, pages 55–74, Washington, DC, USA, 2002. IEEE
Computer Society.
ISBN 0-7695-1483-9.
URL <http://dl.acm.org/citation.cfm?id=645683.664578>.