More Like this

1. Nonmalleable Information Flow Control

   https://doi.org/10.1145/3133956.3134054  

   Cecchetti, Ethan; Myers, Andrew C.; Arden, Owen (October 2017, ACM Conference on Computer and Communications Security)

   Noninterference is a popular semantic security condition because it offers strong end-to-end guarantees, it is inherently compositional, and it can be enforced using a simple security type system. Unfortunately, it is too restrictive for real systems. Mechanisms for downgrading information are needed to capture real-world security requirements, but downgrading eliminates the strong compositional security guarantees of noninterference. We introduce _nonmalleable information flow_, a new formal security condition that generalizes noninterference to permit controlled downgrading of both confidentiality and integrity. While previous work on robust declassification prevents adversaries from exploiting the downgrading of confidentiality, our key insight is _transparent endorsement_, a mechanism for downgrading integrity while defending against adversarial exploitation. Robust declassification appeared to break the duality of confidentiality and integrity by making confidentiality depend on integrity, but transparent endorsement makes integrity depend on confidentiality, restoring this duality. We show how to extend a security-typed programming language with transparent endorsement and prove that this static type system enforces nonmalleable information flow, a new security property that subsumes robust declassification and transparent endorsement. Finally, we describe an implementation of this type system in the context of Flame, a flow-limited authorization plugin for the Glasgow Haskell Compiler. 

   more » « less
2. Knowledge-Based Security of Dynamic Secrets for Reactive Programs

   https://doi.org/10.1109/CSF.2018.00020  

   McCall, McKenna; Zhang, Hengruo; Jia, Limin (July 2018, 2018 IEEE 31st Computer Security Foundations Symposium (CSF))

   Scripts on webpages could steal sensitive user data. Much work has been done, both in modeling and implementation, to enforce information flow control (IFC) of webpages to mitigate such attacks. It is common to model scripts running in an IFC mechanism as a reactive program. However, this model does not account for dynamic script behavior such as user action simulation, new DOM element generation, or new event handler registration, which could leak information. In this paper, we investigate how to secure sensitive user information, while maintaining the flexibility of declassification, even in the presence of active attackers-those who can perform the aforementioned actions. Our approach extends prior work on secure-multi-execution with stateful declassification by treating script-generated content specially to ensure that declassification policies cannot be manipulated by them. We use a knowledge-based progress-insensitive definition of security and prove that our enforcement mechanism is sound. We further prove that our enforcement mechanism is precise and has robust declassification (i.e. active attackers cannot learn more than their passive counterpart). 

   more » « less
3. Type-Based Declassification for Free

   https://doi.org/10.1007/978-3-030-63406-3_11  

   Ngo, Minh; Naumann, David A; Rezk, Tamara (January 2020, 22d International Conference on Formal Engineering Methods)

   null (Ed.)

   This work provides a study to demonstrate the potential of using off-the-shelf programming languages and their theories to build sound language-based-security tools. Our study focuses on information flow security encompassing declassification policies that allow us to express flexible security policies needed for practical requirements. We translate security policies, with declassification, into an interface for which an unmodified standard typechecker can be applied to a source program---if the program typechecks, it provably satisfies the policy. Our proof reduces security soundness---with declassification---to the mathematical foundation of data abstraction, Reynolds' abstraction theorem. 

   more » « less
4. CYBER-PHYSICAL SECURITY OF AIR TRAFFIC SURVEILLANCE SYSTEMS

   Thudimilla, Anusha; McMillin, Bruce (March 2020, Critical Infrastructure Protection XIV)

   Cyber-physical system security is a significant concern in the critical infrastructure. Strong interdependencies between cyber and physical components render cyber-physical systems highly susceptible to integrity attacks such as injecting malicious data and projecting fake sensor measurements. Traditional security models partition cyber-physical systems into just two domains – high and low. This absolute partitioning is not well suited to cyber-physical systems because they comprise multiple overlapping partitions. Information flow properties, which model how inputs to a system affect its outputs across security partitions, are important considerations in cyber-physical systems. Information flows support traceability analysis that helps detect vulnerabilities and anomalous sources, contributing to the implementation of mitigation measures. This chapter describes an automated model with graph-based information flow traversal for identifying information flow paths in the Automatic Dependent Surveillance-Broadcast (ADS-B) system used in civilian aviation, and subsequently partitioning the flows into security domains. The results help identify ADS-B system vulnerabilities to failures and attacks, and determine potential mitigation measures. 

   more » « less
5. Validating the Integrity of Audit Logs Against Execution Repartitioning Attacks

   https://doi.org/10.1145/3460120.3484551  

   Yagemann, Carter; Noureddine, Mohammad A.; Hassan, Wajih Ul; Chung, Simon; Bates, Adam; Lee, Wenke (November 2021, 2021 ACM SIGSAC Conference on Computer and Communications Security)

   Provenance-based causal analysis of audit logs has proven to be an invaluable method of investigating system intrusions. However, it also suffers from dependency explosion, whereby long-running processes accumulate many dependencies that are hard to unravel. Execution unit partitioning addresses this by segmenting dependencies into units of work, such as isolating the events that processed a single HTTP request. Unfortunately, we discover that current designs have a semantic gap problem due to how system calls and application log messages are used to infer complex internal program states. We demonstrate how attackers can modify existing code exploits to control event partitioning, breaking links in the attack and framing innocent users. We also show how our techniques circumvent existing program and log integrity defenses. We then propose a new design for execution unit partitioning that leverages additional runtime data to yield verified partitions that resist manipulation. Our design overcomes the technical challenges of minimizing additional overhead while accurately connecting low level code instructions to high level audit events, in part with the use of commodity hardware processor tracing. We implement a prototype of our design for Linux, MARSARA, and extensively evaluate it on 14 real-world programs, targeted with expertly crafted exploits. MARSARA's verified partitions successfully capture all the attack provenances while only reintroducing 2.82% of false dependencies, in the worst case, with an average overhead of 8.7%. Using a new metric called Partitioning Attack Surface, we show that MARSARA eliminates 47,642 more repartitioning gadgets per program than integrity defenses like CFI, demonstrating our prototype's effectiveness and the novelty of the attacks it prevents. 

   more » « less