Hello everyone:
I noticed an abstract specification of the CapDL initialiser in the SysInit proofs, however i could not find a refinement proof between the abstract specification and the provided c implementation in seL4/capdl/capdl-loader-app.
I wonder if the refinement is in progress, or if there is some significant challenge blocking this.
Background: i am planning to implement and verify a simplified prototype of Execution Management in AUTOSAR AP directly on top of seL4 objects as my graduate thesis. Roughly speaking, it’s just a process manager that launches processes according to given dependency topology, and handles requests on process lifecycle management operations. I wonder whether could i make it feasible after all by simplifying the design and introducing assumptions to bypass the challenging gaps like the Kernel-Userland gap.