Thank you Japheth and Gerwin for your clarification; I didnt know that the glue code proof is no longer maintained in CAmkES. I think assuming the CAmkES interface (we only need RPC-s for our trusted component) works in our case. We are going to manually adapt the proof from the technical report and fit in into our C code first. I will definitely let you guys know if I have time (and feel more confident) on updating the proof to the current version of CAmkES. Best, Oak On Tue, Oct 1, 2019 at 8:47 PM Klein, Gerwin (Data61, Kensington NSW) < Gerwin.Klein@data61.csiro.au> wrote:
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
-- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine