[cap-talk] Haskell @inert-like construct

[Tyler Close]

Hi Toby,

Answers inline below...

On Wed, Sep 3, 2008 at 1:26 AM, Toby Murray <toby.murray at comlab.ox.ac.uk> wrote:
> On Tue, 2008-09-02 at 17:40 -0700, Tyler Close wrote:
>> 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.
>
>> 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.
>
> Does the encode() method being functionally pure not guarantee these
> properties?

Neither ConstArray, nor Exporter are Immutable, so the method is not
functionally pure.

>> I proposed the @inert auditor.
>
> I remember reading the description of the @inert auditor when it was
> first posted to e-lang. Both times I've failed to understand what it's
> doing, based on the rules the verifier is enforcing. Can you elaborate
> further?

As you pointed out above, the two properties of interest would be
trivially true if the encode() method was functionally pure.
Unfortunately, the data structure we want to generate a JSON text for
is not Immutable; it must be able to contain references to mutable
objects. Although the data structure contains mutable state, the
encode() method doesn't actually need to read or write this mutable
state in order to generate the JSON text, instead a URL reference is
assigned to those places. The purpose of the @inert annotation is to
declare to the Joe-E verifier that no mutable state will be read or
written via a particular variable. The proposed rules for the @inert
annotation enforce this constraint. So, going back to the declaration
of the encode() method, the @inert annotation colloquially says:
"Although we're passing in a reference to some mutable state, the
implementation won't touch it". The encode() method is now almost
functionally pure, except for the Exporter argument. This assurance is
good enough that we can ignore the implementation of encode() and just
look at the implementation of the given Exporter.

>> 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);
>
> Again, I've failed to understand the crucial difference between the
> correct and incorrect cases here. Could you explain further why the
> second cases are invalid and what property is being enforced here?

With the encode() method, we just want to check that we're traversing
a data structure safely. Another common use case will be assembling a
data structure safely. For example, in the code above we're proving
that constructing a Foo has no effect on the referenced "x" member.

--Tyler