Hi Oak,

> On 2 Oct 2019, at 11:54, Lim, Japheth (Data61, Kensington NSW) <Japheth.Lim@data61.csiro.au> wrote:
>
>> Roughly speaking, our plan is to use: (1) Isabelle theorems generated
>> by the CapDL capability distribution framework to prove isolation of
>> the user-space and (2) the CAmkES generated Isabelle theorems to prove
>> functional correctness of our security-critical user-space process.
>> The operations of our security-critical process should be simple and
>> similar to the quoting enclave in SGX
>
> If the program is simple, it might be feasible to perform the relevant
> proofs by hand. One difficulty is that the latest C glue code might not
> conform to our formal C subset and would need to be tweaked. Aside from
> that, the proofs should be conceptually similar.


Japheth is correct, of course, but another valid choice would be to just assume the CAmkES interface in your proofs in the style of the report that you found, so that the proof would compose if the glue code proofs still worked.

In addition, depending on what you are trying to verify, the architecture proofs tend to be more important than the glue code proofs for security and isolation, which is one of the reasons the proof of concept for the glue code proofs has not been maintained.

We do have plans to get back to CAmkES glue code proofs in C again eventually, we are just busy on the CakeML side at the moment, and don’t have a concrete time line. Probably some time in 2020, but it depends on a number of factors.

If you are interested in looking at these yourself and potentially updating them, let us know.

Cheers,
Gerwin