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) < [email protected]> wrote: > Hi Oak, > > > On 2 Oct 2019, at 11:54, Lim, Japheth (Data61, Kensington NSW) < > [email protected]> 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
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
