26 citations · 55 across the 11 of their papers we have counts for
12 papers
Bao: Automatic Region Placement and Memory Allocation for Intermittent Computing
Byeongjee Kang, Jan Hoffmann, Limin Jia +2
Intermittent computing enables batteryless embedded devices to operate in harsh environment, but frequent power failures interrupt program execution and require careful management…
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…
Towards a Formal Foundation of Intermittent Computing
Milijana Surbatovich, Limin Jia, Brandon Lucia
Intermittently powered devices enable new applications in harsh or inaccessible environments, such as space or in-body implants, but also introduce problems in programmability and…
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…
A Program Logic for Verifying Secure Routing Protocols
Chen Chen, Limin Jia, Hao Xu +3
The Internet, as it stands today, is highly vulnerable to attacks. However, little has been done to understand and verify the formal security guarantees of proposed secure inter-do…
Equivalence-based Security for Querying Encrypted Databases: Theory and Application to Privacy Policy Audits
Omar Chowdhury, Deepak Garg, Limin Jia +1
Motivated by the problem of simultaneously preserving confidentiality and usability of data outsourced to third-party clouds, we present two different database encryption schemes t…
System M: A Program Logic for Code Sandboxing and Identification
Limin Jia, Shayak Sen, Deepak Garg +1
Security-sensitive applications that execute untrusted code often check the code's integrity by comparing its syntax to a known good value or sandbox the code to contain its effect…
A Logical Method for Policy Enforcement over Evolving Audit Logs
Deepak Garg, Limin Jia, Anupam Datta
We present an iterative algorithm for enforcing policies represented in a first-order logic, which can, in particular, express all transmission-related clauses in the HIPAA Privacy…