Trust and Verify: Formally Verified and Upgradable Trusted Functions
Computation over sensitive data requires that the computation function is secure and trusted. Existing approaches either do not enforce formal verification, require the user to verify the proof, or lack secure attestation guarantees. In addition, neither addresses the issue of having users once again inspect the application after upgrading the code running in the enclave.
We propose an approach that uses a formal specification to guarantee that the behavior of the computation function conforms to the desired functionality. By combining automated verification with attestation on a trusted execution environment, we ensure that only conformant applications are executed. At the same time, we allow updates of the computation function without changing the attestation response, as long as the formal specification still holds. We implement and evaluate the system on several functions; our results show an average overhead of only 50%. Finally, we demonstrate the validity of the system using a real-world application, Dafny-EVM.
Fri 12 SepDisplayed time zone: Auckland, Wellington change
13:30 - 15:00 | Session 16 - Security 2Research Papers Track / Industry Track / Registered Reports / NIER Track at Case Room 2 260-057 Chair(s): Gregorio Robles Universidad Rey Juan Carlos | ||
13:30 15m | Understanding the Faults in Serverless Computing Based Applications: An Empirical Study Research Papers Track Changrong Xie National University of Defense Technology, Yang Zhang National University of Defense Technology, China, Xinjun Mao National University of Defense Technology, Kang Yang National University of Defense Technology, Tanghaoran Zhang National University of Defense Technology | ||
13:45 15m | Security Vulnerabilities in Docker Images: A Cross-Tag Study of Application Dependencies Research Papers Track Hamid Mohayeji Nasrabadi Eindhoven University of Technology, Eleni Constantinou University of Cyprus, Alexander Serebrenik Eindhoven University of Technology | ||
14:00 15m | Trust and Verify: Formally Verified and Upgradable Trusted Functions Research Papers Track Marcus Birgersson KTH Royal Institute of Technology, Cyrille Artho KTH Royal Institute of Technology, Sweden, Musard Balliu KTH Royal Institute of Technology | ||
14:25 10m | MalLoc: Towards Fine-grained Android Malicious Payload Localization via LLMs NIER Track Tiezhu Sun University of Luxembourg, Marco Alecci University of Luxembourg, Aleksandr Pilgun University of Luxembourg, Yewei Song University of Luxembourg, Xunzhu Tang University of Luxembourg, Jordan Samhi University of Luxembourg, Luxembourg, Tegawendé F. Bissyandé University of Luxembourg, Jacques Klein University of Luxembourg Pre-print | ||
14:35 15m | Levels of Binary Equivalence for the Comparison of Binaries from Alternative Builds Industry Track Jens Dietrich Victoria University of Wellington, Tim White Victoria University of Wellington, Behnaz Hassanshahi Oracle Labs, Australia, Paddy Krishnan Oracle Labs, Australia | ||
14:50 10m | Repairing vulnerabilities without invisible hands. A differentiated replication study on LLMs Registered Reports Maria Camporese University of Trento, Fabio Massacci University of Trento; Vrije Universiteit Amsterdam | ||