sophiaIC
commented
3 years ago Thank you for the pointer to the CSF paper. No, we are not using Iris. Iris is very powerful, and accommodates separation logic, but so far, we are not using separation logic, so have no need for Iris, even though in future we might need to introduce some version of it.
The CSF paper is proposing to express the properties of wrappers as properties of traces. We have tried this in the past as part of a Master’s project at imperial, but found this a bit cumbersome, as it required us to break traces into subtrades. The current version (not published yet) is far more direct.
cc @JulianMackayhttps://github.com/JulianMackay @erightshttps://github.com/erights
Sophia Drossopoulou https://wp.doc.ic.ac.uk/sd/
From: Dan Connolly @.> Date: Monday, 9 August 2021 at 18:21 To: sophiaIC/HolisticSpecifications @.> Cc: Subscribed @.> Subject: [sophiaIC/HolisticSpecifications] considered Iris? (#2) This email from @. originates from outside Imperial. Do not click on links and attachments unless you recognise the sender. If you trust the sender, add them to your safe senders listhttps://spam.ic.ac.uk/SpamConsole/Senders.aspx to disable email stamping for this address.
Have you considered using Irishttps://iris-project.org/? (It's possible that you are and I just can't read Coq code well enough to know, but it doesn't look like it.)
The reason I ask is that I just read another relevant paper that uses it...
Capability-based systems support the enforcement of security properties in the presence of arbitrary untrusted code in the system through what are typically called object capability patterns, like the membrane or caretaker patterns [31]. It is only relatively recently that sufficiently powerful formal reasoning approaches have been developed that can prove such properties. Devriese et al. [7] proposed a reasoning approach based on logical relations, (what we now call) universal contracts and the concept of effect parametricity. Swasey et al. [8] developed the first program logic, OCPL, that can compositionally specify and verify the properties enforced by object capability patterns. Building on these ideas, program logics have been developed to reason about software in low-level capability-based instruction set architectures [10], [11]. These logics, as ours, are built in Iris [18], a separation logic framework for building program logics. Iris integrates, unifies, and simplifies a wide variety of mechanisms for reasoning about programs that can be higher order, concurrent, or use mutable state
- Proving Full-System Security Properties under Multiple Attacker Models on Capability Machineshttps://cs.au.dk/~birke/papers/caps-mmio-conf.pdf. T. Van Strydonck, A.L. Georges, A. Gueneau, A. Trieu, A. Timany, F. Piessens, L. Birkedalhttps://cs.au.dk/~birke/papers/index.html, and D. Devriese. In CSF 2022: Computer Security Foundations
cc @JulianMackayhttps://github.com/JulianMackay @erightshttps://github.com/erights
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/sophiaIC/HolisticSpecifications/issues/2, or unsubscribehttps://github.com/notifications/unsubscribe-auth/ABULC4MA75STPIH4ITPH7DDT37XBHANCNFSM5B2H4AUA. Triage notifications on the go with GitHub Mobile for iOShttps://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Androidhttps://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email.
dckc
Have you considered using Iris? (It's possible that you are already using it and I just can't read Coq code well enough to know, but it doesn't look like it.)
The reason I ask is that I just read another relevant paper that uses it...
T. Van Strydonck, A.L. Georges, A. Gueneau, A. Trieu, A. Timany, F. Piessens, L. Birkedal, and D. Devriese. In CSF 2022: Computer Security Foundations
cc @JulianMackay @erights