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
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