On Tue, Aug 27, 2019 at 9:24 AM Norrathep Rattanavipanon <
nrattana@uci.edu> 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
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.
-- 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