Hi,
I have been reading Andrew Boyton's thesis about CapDL and realized that CapDL does not support a shared memory page. Is it still a limitation in CapDL/Camkes? Or has it somehow been addressed?
Does this limitation include the case where a page is mapped/shared with different access rights? e.g., a page is mapped writable to one process and the same page is mapped only readable to another process?
Best, Norrathep
Hi Norrathep,
I have been reading Andrew Boyton's thesis about CapDL and realized that CapDL does not support a shared memory page. Is it still a limitation in CapDL/Camkes? Or has it somehow been addressed?
This limitation has been lifted recently on the verification side, there can now be more than one cap to a frame in capDL.
I believe this has already made it into the public master branch, but I haven’t checked. If I remember correctly, the rest of the capDL tool chain has had this ability for quite some time, the result would just not pass wellformedness verification.
Does this limitation include the case where a page is mapped/shared with different access rights? e.g., a page is mapped writable to one process and the same page is mapped only readable to another process?
The different caps to the same frame can have different access rights, i.e. your scenario should be possible.
Cheers, Gerwin
Thanks for the reply, Gerwin. I really appreciate it. I have further questions below.
On Sun, Aug 4, 2019 at 8:51 PM Klein, Gerwin (Data61, Kensington NSW) < Gerwin.Klein@data61.csiro.au> wrote:
Hi Norrathep,
I have been reading Andrew Boyton's thesis about CapDL and realized that
CapDL does not support a shared memory page. Is it still a limitation in CapDL/Camkes? Or has it somehow been addressed?
This limitation has been lifted recently on the verification side, there can now be more than one cap to a frame in capDL.
I believe this has already made it into the public master branch, but I haven’t checked. If I remember correctly, the rest of the capDL tool chain has had this ability for quite some time, the result would just not pass wellformedness verification.
So does it have any implication if it fails wellformedness verification? i.e., would I still be able to extend the Camkes proof to prove functional correctness of the component's code? Btw, how can I access generated Isabelle theorems from Camkes. I'm using Camkes from the public master branch. I think I could access generated glue code and capdl C specification (e.g., for hello-camkes-1 example, it's in hello-camkes-1_build/capdl_spec.c) but I couldnt find any generated RPC stub and system initialization theorems.
Does this limitation include the case where a page is mapped/shared with
different access rights? e.g., a page is mapped writable to one process and the same page is mapped only readable to another process?
The different caps to the same frame can have different access rights, i.e. your scenario should be possible.
Cheers, Gerwin
On 6 Aug 2019, at 05:04, Norrathep Rattanavipanon <nrattana@uci.edumailto:nrattana@uci.edu> wrote:
I believe this has already made it into the public master branch, but I haven’t checked. If I remember correctly, the rest of the capDL tool chain has had this ability for quite some time, the result would just not pass wellformedness verification.
So does it have any implication if it fails wellformedness verification?
Yes, wellformedness is the precondition for the capDL-initialiser proof to apply. If it fails that, there is no proof that the initial system state conforms to the capDL spec. It will happen to conform anyway, but you’d have no proof. That said, shared frames should no longer fail wellformedness in capDL.
i.e., would I still be able to extend the Camkes proof to prove functional correctness of the component's code?
You could still do that separately, but you wouldn’t be able to connect the capDL and the CAmkES proofs. These proofs are not connected at the moment anyway (although we are working towards that).
Btw, how can I access generated Isabelle theorems from Camkes. I'm using Camkes from the public master branch. I think I could access generated glue code and capdl C specification (e.g., for hello-camkes-1 example, it's in hello-camkes-1_build/capdl_spec.c) but I couldnt find any generated RPC stub and system initialization theorems.
I think I should leave that part of the answer to Japheth or someone else from the team, because this is currently in flux. We’re busy extending the whole setup to be more flexible so that it applies to more systems (i.e. useful systems). This also slightly changes how everything works together, how things are generated etc.
Cheers, Gerwin
On Mon, Aug 5, 2019 at 3:26 PM Klein, Gerwin (Data61, Kensington NSW) < Gerwin.Klein@data61.csiro.au> wrote:
On 6 Aug 2019, at 05:04, Norrathep Rattanavipanon nrattana@uci.edu wrote:
I believe this has already made it into the public master branch, but I haven’t checked. If I remember correctly, the rest of the capDL tool chain has had this ability for quite some time, the result would just not pass wellformedness verification.
So does it have any implication if it fails wellformedness verification?
Yes, wellformedness is the precondition for the capDL-initialiser proof to apply. If it fails that, there is no proof that the initial system state conforms to the capDL spec. It will happen to conform anyway, but you’d have no proof. That said, shared frames should no longer fail wellformedness in capDL.
i.e., would I still be able to extend the Camkes proof to prove functional correctness of the component's code?
You could still do that separately, but you wouldn’t be able to connect the capDL and the CAmkES proofs. These proofs are not connected at the moment anyway (although we are working towards that).
Btw, how can I access generated Isabelle theorems from Camkes. I'm using Camkes from the public master branch. I think I could access generated glue code and capdl C specification (e.g., for hello-camkes-1 example, it's in hello-camkes-1_build/capdl_spec.c) but I couldnt find any generated RPC stub and system initialization theorems.
I think I should leave that part of the answer to Japheth or someone else from the team, because this is currently in flux. We’re busy extending the whole setup to be more flexible so that it applies to more systems (i.e. useful systems). This also slightly changes how everything works together, how things are generated etc.
I look forward to knowing that. I'm also interested in the C refinement proof (of the initializer) in CapDL. I tried to look into l4v repo in: https://github.com/seL4/l4v/tree/master/proof/crefine and https://github.com/seL4/l4v/blob/master/sys-ini. But I couldnt find it. If anyone can give me a pointer, I'd really appreciate it.
Cheers, Gerwin
Hi Norrathep,
Btw, how can I access generated Isabelle theorems from Camkes. I'm using Camkes from the public master branch. I think I could access generated glue code and capdl C specification (e.g., for hello-camkes-1 example, it's in hello-camkes-1_build/capdl_spec.c) but I couldnt find any generated RPC stub and system initialization theorems.
I think I should leave that part of the answer to Japheth or someone else from the team, because this is currently in flux. We’re busy extending the whole setup to be more flexible so that it applies to more systems (i.e. useful systems). This also slightly changes how everything works together, how things are generated etc.
I look forward to knowing that. I'm also interested in the C refinement proof (of the initializer) in CapDL. I tried to look into l4v repo in: https://github.com/seL4/l4v/tree/master/proof/crefine and https://github.com/seL4/l4v/blob/master/sys-ini. But I couldnt find it. If anyone can give me a pointer, I'd really appreciate it.
There is currently no C-level proof of the initialiser, the proof is on the model level (model = spec of the initialiser) only. The initial plan was indeed to perform a refinement down towards C, but we have in the meantime changed plans and are looking into getting that implementation in CakeML instead, which comes with its own compiler proof and is hopefully much easier to connect to the initialiser semantics in Isabelle. This is ongoing work.
Cheers, Gerwin
-
Klein, Gerwin (Data61, Kensington NSW) -
Norrathep Rattanavipanon