Polymorphic Information-flow Guards — Guardies

Guardies is currently developed in the Department of Computer Science of the University of Liverpool by Nicolas Berthier, in collaboration with Narges Khakpour from the Department of Computer Science and Media Technology at Linnaeus University.

This work started as a new approach to Narges' previous work in the PROSSES project.

The working principles of Guardies are as follows:

• Input methods are given in an assembly-style object-oriented language very similar to Soot's Jimple language, that closely reflects Java bytecode. This allows Guardies to handle already compiled and optimized applications (e.g. jar, apk);
• Each method is considered separately and its security semantics is encoded using a symbolic transition system. This encoding assigns security levels to variables and reachable portions of heap, and encodes the control-flow of the method under consideration. It involves a generic symbolic abstract heap domain to capture relations between reference variables, as well as direct and indirect information flow through object mutations;
• Information-flow properties (such as data confidentiality or integrity) are then translated into safety properties on the system;
• Lastly, a co-reachability analysis solver is used to infer a sound polymorphic information-flow guard for the method, that expresses circumstances upon which the method satisfies the in terms of its calling context (i.e. security levels and relations pertaining to its formal arguments).

Guardies relies on ReaTK to solve the symbolic discrete controller synthesis problems.

The tool will be distributed under the terms of the GNU General Public License upon appearance of a first publication about the underlying approach.

Security levels belong to the set \(\{⊥,⊤\}\). \(⊥\) denotes low or public level, and \(⊤\) denotes high or private level. \(⊔\) is the least upper bound between two security levels (i.e. in our case, \(a ⊔ b = ⊤\) iff \(a = ⊤\) or \(b = ⊤\)). The inferred security summaries involve the security level of variables (noted level(v) for a primitive or reference variable v) as well as of potentially reachable objects (denoted obj_level(r) for a reference variable r).

Furthermore, pc denotes the security level of the calling context for a method.

Guardies makes use of a generic notion of symbolic abstract heap domain to represent heap abstractions as part of the encoding of security semantics. The chosen domain impacts the precision and cost of the analysis, as well as the set of relations that may appear in guards inferred by the tool.

Several kinds of symbolic variables pertaining to reference variables may appear in guards inferred by Guardies. The descriptions bellow assume the domain named "deep" is used, which involves the following Heap-related relations. Given two reference variables a and b, a~b denotes that \(\vec{a}\) and \(\vec{b}\) may be the same object (i.e. a and b may alias). Similarly, a.~>b denotes that a field (or cell) of \(\vec{a}\) may (transitively) reference \(\vec{b}\).

Let's assume given a complete class hierarchy, and a method m for which we want to compute a security summary. Listing 1 presents a description of object types as understood by Guardies, where class A directly extends java.lang.Object and does not declare any field, class B inherits from A and features a primitive field f of type int, and class C are objects that may reference objects of the same class through a field f.

A <: java.lang.Object
B <: A { int f; }
C <: java.lang.Object { C f; }

Sets of security stubs can be given to Guardies in files with extension .secstubs. Such a file associates method type signatures with possibly empty sequences of statements. For each one of these associations, these statements are used by the tool to construct information-flow guards and effect transformers, which put together form a summary for the method, in the following way:

• First, a default summary is built based on a few characteristics of the method (whether it is static or not, or whether it is a constructor, whether it returns a reference, and the type of its arguments)—See Section Defaults below;
• Then, the sequence of statements in the security stub is processed sequentially to iteratively amend the summary—See Section Statements;
• The resulting summary is then associated with the method and is later treated by Guardies as if it had been computed from an implementation of the method itself.

Listings 8 and 10 illustrate the construction of summaries from stubs by means of amending the default.

/* None of the following methods perform any mutation */
int A:nice1 (C, C, int) { -<~; return new }
int A:nice2 (C, C, int) { -<~; return @ }
C A:nice_allocC (C, C, int) { -<~; return new }
void A:nice_log (C, int) { -<~; output_⊥ }

int A:nice1 (C a0, C a1, int a2) {
  guard = tt;
  ret(level()) = ⊥;
  ret(obj_level(a0)) = obj_level(a0);
  ret(obj_level(a1)) = obj_level(a1);
  ret(obj_level(this)) = obj_level(this);
  ret(a0.~>a0) = a0.~>a0;
  ret(a0.~>a1) = a0.~>a1;
  ret(a1.~>a0) = a1.~>a0;
  ret(a1.~>a1) = a1.~>a1;
}
int A:nice2 (C a0, C a1, int a2) {
  guard = tt;
  ret(level()) = level(a0) ⊔ level(a1) ⊔ level(a2) ⊔ level(this) ⊔ obj_level(a0) ⊔ obj_level(a1) ⊔ obj_level(this);
  ret(obj_level(a0)) = obj_level(a0);
  ret(obj_level(a1)) = obj_level(a1);
  ret(obj_level(this)) = obj_level(this);
  ret(a0.~>a0) = a0.~>a0;
  ret(a0.~>a1) = a0.~>a1;
  ret(a1.~>a0) = a1.~>a0;
  ret(a1.~>a1) = a1.~>a1;
}
C A:nice_allocC (C a0, C a1, int a2) {
  guard = tt;
  ret(level()) = ⊥;
  ret(obj_level()) = (if ret(~a0) then obj_level(a0) else ⊥) ⊔ (if ret(~a1) then obj_level(a1) else ⊥) ⊔ (if ret(a0.~>) then obj_level(a0) else ⊥) ⊔ (if ret(a1.~>) then obj_level(a1) else ⊥);
  ret(obj_level(a0)) = obj_level(a0);
  ret(obj_level(a1)) = obj_level(a1);
  ret(obj_level(this)) = obj_level(this);
  ret(~a0) = ff;
  ret(~a1) = ff;
  ret(.~>a0) = tt;
  ret(.~>a1) = tt;
  ret(a0.~>) = ff;
  ret(a0.~>a0) = a0.~>a0;
  ret(a0.~>a1) = a0.~>a1;
  ret(a1.~>) = ff;
  ret(a1.~>a0) = a1.~>a0;
  ret(a1.~>a1) = a1.~>a1;
}
void A:nice_log (C a0, int a1) {
  guard = pc ⊑ ⊥ ∧ level(a0) ⊔ level(a1) ⊔ level(this) ⊔ obj_level(a0) ⊔ obj_level(this) ⊑ ⊥;
  ret(obj_level(a0)) = obj_level(a0);
  ret(obj_level(this)) = obj_level(this);
  ret(a0.~>a0) = a0.~>a0;
}

The resulting summaries are given in Listings 9 and 11, respectively.

Observe for instance how the summary for method C A:nice_allocC (C, C, int) indicates that the reference it returns cannot alias any of its arguments of type C.

/* The following method may mutate any of its arguments with public data */
void A:mutate_arg (C, int) { -<~; @<~⊥ }

/* The following method may mutate any of its arguments with any data it
   recieves, and return anything */
A A:mutate_args (A, C, int) { -<~; @<~@; return * }

void A:mutate_arg (C a0, int a1) {
  guard = tt;
  ret(obj_level(a0)) = pc;
  ret(obj_level(this)) = obj_level(this);
  ret(a0.~>a0) = tt;
}
A A:mutate_args (A a0, C a1, int a2) {
  guard = tt;
  ret(level()) = pc ⊔ level(a0) ⊔ level(a1) ⊔ level(a2) ⊔ level(this) ⊔ obj_level(a0) ⊔ obj_level(a1) ⊔ obj_level(this);
  ret(obj_level()) = pc ⊔ level(a0) ⊔ level(a1) ⊔ level(a2) ⊔ level(this) ⊔ obj_level(a0) ⊔ obj_level(a1) ⊔ obj_level(this) ⊔ (if ret(~a0) then obj_level(a0) else ⊥) ⊔ (if ret(~this) then obj_level(this) else ⊥);
  ret(obj_level(a0)) = pc ⊔ level(a0) ⊔ level(a1) ⊔ level(a2) ⊔ level(this) ⊔ obj_level(a0) ⊔ obj_level(a1) ⊔ obj_level(this);
  ret(obj_level(a1)) = pc ⊔ level(a0) ⊔ level(a1) ⊔ level(a2) ⊔ level(this) ⊔ obj_level(a0) ⊔ obj_level(a1) ⊔ obj_level(this);
  ret(obj_level(this)) = obj_level(this);
  ret(~a0) = tt;
  ret(~this) = tt;
  ret(a1.~>a1) = tt;
}

Note that users wanting to handle exceptions when processing .meth files must give the corresponding translation flag (with `-tf +exceptions' on the command-line) before feeding Guardies with a set of security stubs (similarly for taints…). Doing so for the stubs of Listing 6 produces default-w-exceptions.secsums.