Next paper 18 August

data/desc.txt

@@ -1,3 +1,3 @@
-ILC: a calculus for composable, computational cryptography
-Liao, Kevin, et al. “ILC: A Calculus for Composable, Computational Cryptography.” Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2019. Crossref, https://doi.org/10.1145/3314221.3314607.
-https://doi.org/10.1145/3314221.3314607
+VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A
+Liu, Zongyuan, et al. “VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 1438–62. Crossref, https://doi.org/10.1145/3591279.
+Thin hypervisors make it possible to isolate key security components like keychains, fingerprint readers, and digital wallets from the easily-compromised operating system. To work together, virtual machines running on top of the hypervisor can make hypercalls to the hypervisor to share pages between each other in a controlled way. However, the design of such hypercall ABIs remains a delicate balancing task between conflicting needs for expressivity, performance, and security. In particular, it raises the question of what makes the specification of a hypervisor, and of its hypercall ABIs, good enough for the virtual machines. In this paper, we validate the expressivity and security of the design of the hypercall ABIs of Arm's FF-A. We formalise a substantial fragment of FF-A as a machine with a simplified ISA in which hypercalls are steps of the machine. We then develop VMSL, a novel separation logic, which we prove sound with respect to the machine execution model, and use it to reason modularly about virtual machines which communicate through the hypercall ABIs, demonstrating the hypercall ABIs' expressivity. Moreover, we use the logic to prove robust safety of communicating virtual machines, that is, the guarantee that even if some of the virtual machines are compromised and execute unknown code, they cannot break the safety properties of other virtual machines running known code. This demonstrates the intended security guarantees of the hypercall ABIs. All the results in the paper have been formalised in Coq using the Iris framework.

data/history.txt

@@ -7,4 +7,5 @@ https://doi.org/10.1145/3571239
 https://doi.org/10.1145/3571204
 https://doi.org/10.1145/3571211
 https://doi.org/10.1145/3547652
-https://doi.org/10.1145/3314221.3314607
+https://doi.org/10.1145/3314221.3314607
+https://doi.org/10.1145/3591279

data/next.txt

@@ -1 +1 @@
-https://doi.org/10.1145/3314221.3314607
+https://doi.org/10.1145/3591279

data/past.txt

@@ -1,2 +1,3 @@
 
-https://doi.org/10.1145/3314221.3314607
+https://doi.org/10.1145/3314221.3314607
+https://doi.org/10.1145/3591279

docs/next.md

@@ -1 +1 @@
-Liao, Kevin, et al. “ILC: A Calculus for Composable, Computational Cryptography.” Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2019. Crossref, <a href='https://doi.org/10.1145/3314221.3314607' target='_blank'>https://doi.org/10.1145/3314221.3314607</a>.
+Liu, Zongyuan, et al. “VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 1438–62. Crossref, <a href='https://doi.org/10.1145/3591279' target='_blank'>https://doi.org/10.1145/3591279</a>.

docs/papers.md

@@ -1 +1,2 @@
-1. Liao, Kevin, et al. “ILC: A Calculus for Composable, Computational Cryptography.” Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2019. Crossref, <a href='https://doi.org/10.1145/3314221.3314607' target='_blank'>https://doi.org/10.1145/3314221.3314607</a>.
+1. Liu, Zongyuan, et al. “VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A.” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, June 2023, pp. 1438–62. Crossref, <a href='https://doi.org/10.1145/3591279' target='_blank'>https://doi.org/10.1145/3591279</a>.
+2. Liao, Kevin, et al. “ILC: A Calculus for Composable, Computational Cryptography.” Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, June 2019. Crossref, <a href='https://doi.org/10.1145/3314221.3314607' target='_blank'>https://doi.org/10.1145/3314221.3314607</a>.