6 papers
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…
Containing Malicious Package Updates in npm with a Lightweight Permission System
Gabriel Ferreira, Limin Jia, Joshua Sunshine +1
The large amount of third-party packages available in fast-moving software ecosystems, such as Node.js/npm, enables attackers to compromise applications by pushing malicious update…
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,…
Uncovering Information Flow Policy Violations in C Programs
Darion Cassel, Yan Huang, Limin Jia
Programmers of cryptographic applications written in C need to avoid common mistakes such as sending private data over public channels, modifying trusted data with untrusted functi…