Hello Japheth, What I'm missing is the generated theorems provided by CAmkES. I'm looking for something similar to chapter 5 and Appendix B of this technical report: https://ts.data61.csiro.au/publications/nicta_full_text/9034.pdf. I couldn't find it anywhere when building the CAmKES tutorial project. Can you give me a pointer on how to generate that? Please see below for more information about our work and my further questions. On Tue, Aug 27, 2019 at 9:24 AM Norrathep Rattanavipanon wrote:

Thanks Japheth. I confirmed that I can generate Isabelle files from camkes by modifying the camkes setting. I haven't tried with generated proof for glue code. Will let you know if I have more question.

Thanks

On Wed, Aug 21, 2019, 12:24 AM Lim, Japheth (Data61, Kensington NSW) < Japheth.Lim@data61.csiro.au> wrote:

...

Hi Norrathep,

Norrathep Rattanavipanon wrote:

...

I have been trying to generate Isabelle file from CapDL specification. But I run into an error when I'm running the command:

./parse-capDL --isabelle=out.thy --object-sizes=object_sizes.yaml example-arm.cdl

We recently put in a major change to the Isabelle translator. The input capDL file is now required to be pre-allocated, i.e. every object must be placed in an untyped with a known physical address.

The existing example files date from before this change, and so they don't meet the requirements to be translated into Isabelle. Sorry that you got confusing error messages as a result. We plan to make this more consistent in the near future.

...

Is there any step I'm missing? Or does the tool not support the conversion to Isabelle?

The standard way is to build a CAmkES application with the option `CAmkESCapDLStaticAlloc` enabled. This will generate a suitable capDL file for proofs.

Based on your other question thread, you may be interested in our README for CAmkES proofs:

https://github.com/seL4/camkes-tool/tree/master/cdl-refine-tests

This generates proofs between the CAmkES high-level model and the capDL system representation. However, we are not working on C glue code proofs at the moment.

Unless I'm missing something, arent C glue code proofs the same as what is described in chapter 5/Appendix B of the above technical report? In other words, isn't it done by DATA61 already?

...

This is all work in progress, and quite rough around the edges. Nevertheless, we're happy to try to answer any questions you might have. It would help if we knew more about your work, so that we can give more specific replies.

My apologies, I should have mentioned about the work we are doing earlier. Basically, we are looking to verify our earlier work ( http://sprout.ics.uci.edu/projects/attestation/papers/hydra.pdf) -- a security architecture that uses seL4 as a building block to provide memory isolation. In there, we only designed the entire system, without actually verifying it, so we would like to actually finish our work there :). 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: (i) receives a request from the endpoint. The request specifies a memory region that needs to be included in a quote. (ii) creates a quote by hashing all memory contents in the requested region. (iii) returns the quote back to the same endpoint. Our use-case should have a lot of similarities as the example in your technical report and that is why we want to adopt the same methodology when setting up a verification framework. So far, I managed to get Isabelle theorems generated by CapDL but I could not figure out how to get generated CAmkES proofs (similar to the one in chapter 5).

...

Cheers, Japheth Lim Proof Engineer, Trustworthy Systems

Best Regards, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

Hi Oak,

On 2 Oct 2019, at 11:54, Lim, Japheth (Data61, Kensington NSW) 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