[cap-talk] Haskell @inert-like construct

[Tyler Close]

I wasn't expecting this to land on cap-talk just yet, but since Kevin
sent it, I'll add some context.

I've been using different parts of the Waterken Server implementation
as test cases for how to write code in a way that facilitates a
security review. Recently, in a conversation on e-lang, I proposed a
new auditor, @inert, for the Joe-E verifier that might make many
security claims machine verifiable and so require very little human
effort during a security review. For example, consider a JSON
serializer with API:

interface Exporter {
    String run(@inert Object x);
}

static public String
encode(final Exporter export, final @inert ConstArray<?> values);

The encode() method generates a JSON text that represents the
immutable parts of the object tree reachable from the values argument.
The Exporter is used to assign a URL to references to mutable objects.
So you might get an output JSON text like:

[ {
    "$" : "org.example.Pal",
    "petname" : "Alan",
    "inbox" : { "@" : "../alan/#asdfasdf" },
    "nickname" : "Alan Karp"
  } ]

The "inbox" member above refers to an object for sending messages to Alan.

In a security review, it might be important to know a couple things
about the implementation of the encode() method. For example, it might
be important to know that
A. the encode() implementation will not mutate any of the state
reachable via the "values" argument.
B. the output will be the same if you call the method with the same
arguments (important to know if you want to cache the output)

Today, you'd have to manually inspect the implementation of the
encode() method to determine whether or not these properties hold. I
was looking for a way that a security reviewer could know the
properties hold based only on the type signature of the encode()
method, and so ignoring the implementation. This should save a lot of
high value time during a security review. So I proposed the @inert
auditor.

The @inert auditor can be applied to any variable that exists on the
stack, so local variables and method/constructor parameters. For
variables with this annotation, the Joe-E verifier checks that:
1. On access to a field of the referent, the field MUST be final and
the accessed value MUST be assigned to another variable that either:
  a. is the caller's return value
  b. has the @inert annotation,
  c. or is a scalar type,
  d. or is java.lang.String,
  e. or is java.math.BigInteger,
  f. or is java.math.BigDecimal
2. Invocation of a method of the referent is forbidden.
3. If a caller provides an @inert argument to a constructor or method,
the return value MUST be assigned to a variable meeting the same
conditions listed in case 1.
4. A constructor can initialize a field using an @inert argument, but
MUST NOT access that field.

For example, given the following API:

class Foo {
   public final Object x;
   Foo(@inert final Object x) {
       this.x = x;
   }
}

static public Foo
bar(@inert final Object x) {
   return new Foo(x);
}

the following code is valid:

final Object a = ...
final Foo aFoo = new Foo(a);
final Foo aBar = bar(a);
return new Foo(a);
return bar(a);
final @inert Object b = ...
final @inert Foo bFoo = new Foo(b);
final @inert Foo bBar = bar(b);
return new Foo(b);
return bar(b);

the following code is invalid:

final Foo bFoo = new Foo(b);
final Foo bBar = bar(b);
return new Foo(b);
return bar(b);

Given the above rules, we can determine right away that claim A must
be true. For claim B, we can ignore the implementation of encode(),
since the "values" argument is @inert, and just check that the
Exporter behaves deterministically, always assigning the same URL to
the same object. The @inert auditor also lets me prove a number of
other security claims in the ref_send library. Basically, anytime
you're building up a mutable data structure, or traversing it, the
@inert auditor will let you prove you're doing it in a side-effect
free, repeatable way. An awful lot of code is just building up and
traversing data structures.

Kevin pointed out that the reasoning behind the @inert auditor is sort
of similar to that behind free theorems from generic types in Haskell.
In both cases, you're inferring some properties of a function based on
what it doesn't know. With a generic parameter, the function doesn't
know anything about the argument. With an @inert parameter, the
function doesn't know anything about the argument's mutable state. I
haven't been able to get much more than that out of the comparison,
but then the "Theorems for free" paper is slow reading for me. Anybody
else get anything more out of the comparison?

"Theorems for free - CiteSeerX"
<http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875>

--Tyler

On Tue, Sep 2, 2008 at 4:05 PM, Kevin Reid <kpreid at mac.com> wrote:
> On Sep 2, 2008, at 14:29, Tyler Close wrote:
>
>> Hi Kevin,
>>
>> I want to follow up on your point about the similarity between
>> Haskell's untyped parameters and the @inert annotation. Where's the
>> best place to start reading?
>
> The term is 'parametricity', I believe.
> ( http://en.wikipedia.org/wiki/Parametricity is unfortunately bare.)
>
> They're not exactly untyped; they're of a entirely as-yet-undetermined type.
>
> Suppose we have a function which transforms arbitrary lists in some way; its
> type is, most generally:
>
>  forall a. [a] -> [a]
>
> This is a parametrically polymorphic type - 'a' is a type variable. In any
> particular use of the function, 'a' is bound to some specific type (e.g.
> [Integer] -> [Integer]) -- but the function's type is general, so it cannot
> mention any type-specific operations -- it wouldn't typecheck!
>
> For example, the type of "map (+1)" (which increments every number in a
> list) is *not* [a] -> [a], but rather:
>
>  forall a. Num a => [a] -> [a]
>
> That is, the type variable 'a' is required to be some numeric type. Any
> function having this type must have been verified by the type-checker to not
> contain any operations other than those on lists-in-general and those
> defined by the Num type-class.
>
>
> So Haskell's type system lets you establish arbitrary "do only this
> (possibly empty) subset of operations on these objects" conditions, which in
> an, uh, less-typed system would require wrapping and unwrapping the objects
> to be protected (which becomes especially difficult in the presence of
> complex data structures holding said objects).
>
>
> I asked #haskell for recommendations:
>
> [18:45] <ddarius> kpreid: These behaviours are related to the free theorems,
> so you could look up those as well.
> [18:45] <Saizan_> kpreid: the "theorems for free" of wadler are based on
> parametricity like that
> [18:45] <earthy> http://people.cs.uu.nl/andres/ST-05-2003.pdf are the slides
> of the talk I mentioned
> [18:46] <earthy> but the illustration was in terms of kinder chocolate
> surprise eggs
>
> --
> Kevin Reid                            <http://homepage.mac.com/kpreid/>
>
>
>