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 <[email protected]> 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) < > [email protected]> 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
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
