Security policies are specified in Jalapa through usage automata. They are an extension of finite stata automata, with some additional features that improve their expressivity. These peculiar features are: parameters, wildcards, guards. Below we review the syntax and the semantics of usage automata.
A usage automaton is defined in plain text as follows:
name: policy name aliases: list of aliases (separated by newline) states: list of states (separated by space) start: initial state final: list of offending states (separated by space) trans: list of transitions (separated by newline)
The tag name is the user-defined name of the policy.
The tag aliases defined a mapping from the security-relevant
methods monitored by the policy to the alphabet of the automaton.
An event with name ev and parameters x1,...,xk
is defined as follows:
ev(x1,...,xk) := (y:C).m(C1 y1,...,Cn yn)
Such an event will be fired at run-time, whenever
a method m with signature m(C1 y1,...,Cn yn)
is invoked on an object y of class C.
We require that xj in {y,y1,...,yn}
for all j in 1..k.
Also, x1,...,xk must be pairwise disjoint, as well as
y1,...,yn.
If the number of parameters is zero, one can simply write ev
instead of ev(). If the object y is
not used int the alias, it is possible to write (C)
instead of (y:C).
IMPORTANT: all the class names used in aliases are qualified,
e.g. one writes java.lang.String,
rather than just String.
Note that a usage policy can only control methods known at the time the policy is written. In the case of dynamically loaded code, where methods are only discovered at run-time, it is still possible to specify and enforce policies on statically-known methods. For instance, system resources - which are accessed through the Java API only - can always be protected by policies.
The remaining tags specify the logics of the usage automaton.
The meaning of states, start and final
is the same as for finite state automata, except that in usage automata
with final we denote the states that violate the policy,
that is offending states. The list of transitions following the tag
trans is more peculiar. A transition between two states
q and q' is written as follows:
q -- ev(Z1,...,Zk) --> q' [when cond]
where ev(x1,...,xk) is one of the events defined in the aliases list,
and the Zi can be one of the following:
x, y, ...
"secretfile"
*, meaning "for all possible choices of this object"
-, meaning "for all possible choices of this object, different from everything else mentioned in this policy"
The suffix when cond is optional,
where cond is a boolean condition specified as follows:
cond ::= true | Zi!=Z | cond and cond
where Zi is a formal parameter, and Z is either a static object, or Z is equal to some parameter mentioned in the policy.
A policy that prevents from writing to the disk, after you have read some file:
name: chinese-wall aliases: read := (java.io.BufferedReader).readLine() read := ... // other read methods here write := (java.io.BufferedWriter).write(java.lang.String s, int off, int len) write := ... // other write methods here states: q0 q1 fail start: q0 final: fail trans: q0 -- read --> q1 q1 -- write --> fail
A policy that prevents from writing to the disk, after you have read the file
named confidential:
name: chinese-wall2 aliases: initFR(x,n) := (x:java.io.FileReader).(java.lang.String n) initBR(x,y) := (x:java.io.BufferedReader). (java.io.FileReader y) read(f) := (f:java.io.BufferedReader).readLine() read(f) := ... // other read methods here write := (java.io.BufferedWriter).write(java.lang.String s, int off, int len) write := ... // other write methods here states: q0 q1 q2 q3 fail start: q0 final: fail trans: q0 -- initFR(fr,"confidential") --> q1 q1 -- initBR(br,fr) --> q2 q2 -- read(br) --> q3 q3 -- write --> fail
A policy that prevents from writing to the disk, after you have read any file
different from public1 and public2:
name: chinese-wall3 aliases: initFR(x,n) := (x:java.io.FileReader).(java.lang.String n) initBR(x,y) := (x:java.io.BufferedReader). (java.io.FileReader y) read(f) := (f:java.io.BufferedReader).readLine() read(f) := ... // other read methods here write := (java.io.BufferedWriter).write(java.lang.String s, int off, int len) write := ... // other write methods here states: q0 q1 q2 q3 fail start: q0 final: fail trans: q0 -- initFR(fr,name) --> q1 when name != "public1" q0 -- initFR(fr,name) --> q1 when name != "public2" q1 -- initBR(br,fr) --> q2 q2 -- read(br) --> q3 q3 -- write --> fail
Usage policies constrain the usage of objects to respect a regular property on the program trace, i.e. the sequence of method calls occurred at run-time.
At run-time,
the enforcement mechanism intercepts each security-relevant method call,
and picks the corresponding event from the aliases list.
For each monitored policy with formal parameters x1,...,xk,
the enforcement mechanism maintains a set of pairs of the form:
((O1,...,Ok),Q)
where O1,...,Ok is a tuple of weak references
to the objects that substitute the formal parameters of the usage automaton,
and Q is the current state of the usage automaton
(actually, Q is a subset of states,
since usage automata can be non-deterministic).
When a new event ev(P1,...,Ph) is fired,
the execution monitor first checks whether some of the objects
in P1,...,Ph is not already known to the mechanism.
If this is the case, then new instantiations with actual parameters
(O1,...,Ok) are considered,
for all the possible combinations of known objects
that respect the types of the formal parameters.
If some of these new instantiations (O1,...,Ok)
has a transition that makes it leave from
the start state upon the event ev(P1,...,Ph), then the
pair ((O1,...,Ok),Q) is added to the configuration of the
enforcement mechanism,
where Q is the state tracked by a "dummy" instantiation
of the usage automaton.
Then, each pair ((O1,...,Ok),Q)
in the configuration of the enforcement mechanism is considered.
If the instantiation of the usage automaton on the actual parameters
(O1,...,Ok) moves to Q' upon the event
ev(P1,...,Ph), then the pair is updated to
((O1,...,Ok),Q').
If none of the pairs of the enforcement mechanism contains an offending state, then the intercepted method call is forwarded to the actual target; otherwise, a security exception is thrown.
When an object is garbage-collected, its occurrences in the state of the enforcement mechanism are reverted to dummies.
Note that weak references are used to avoid interference with the garbage collector. Standard references would prevent the garbage collector from disposing objects referenced by the enforcement mechanism only, so potentially leading to memory exhaustion. An object referenced only by weak references is considered unreachable, so it may be disposed by the garbage collector.
See here for a more formal account of the semantics of usage automata.