4 papers · 1 filter
Session Logical Relations for Noninterference
Farzaneh Derakhshan, Stephanie Balzer, Limin Jia
Information flow control type systems statically restrict the propagation of sensitive data to ensure end-to-end confidentiality. The property to be shown is noninterference, asser…
Automatically Enforcing Fresh and Consistent Inputs in Intermittent Systems
Milijana Surbatovich, Limin Jia, Brandon Lucia
Intermittently powered energy-harvesting devices enable new applications in inaccessible environments. Program executions must be robust to unpredictable power failures, introducin…
On the Generation of Disassembly Ground Truth and the Evaluation of Disassemblers
Kaiyuan Li, Maverick Woo, Limin Jia
When a software transformation or software security task needs to analyze a given program binary, the first step is often disassembly. Since many modern disassemblers have become h…
First-order Gradual Information Flow Types with Gradual Guarantees
Abhishek Bichhawat, McKenna McCall, Limin Jia
Information flow type systems enforce the security property of noninterference by detecting unauthorized data flows at compile-time. However, they require precise type annotations,…