skip to main content


Title: Proving confidentiality in a file system using DISKSEC
SFSCQ is the first file system with a machine-checked proof of security. To develop, specify, and prove SFSCQ, this paper introduces DiskSec, a novel approach for reasoning about confidentiality of storage systems, such as a file system. DiskSec addresses the challenge of specifying confidentiality using the notion of _data noninterference_ to find a middle ground between strong and precise information-flow-control guarantees and the weaker but more practical discretionary access control. DiskSec factors out reasoning about confidentiality from other properties (such as functional correctness) using a notion of _sealed blocks_. Sealed blocks enforce that the file system treats confidential file blocks as opaque in the bulk of the code, greatly reducing the effort of proving data noninterference. An evaluation of SFSCQ shows that its theorems preclude security bugs that have been found in real file systems, that DiskSec imposes little performance overhead, and that SFSCQ's incremental development effort, on top of DiskSec and DFSCQ, on which it is based, is moderate.  more » « less
Award ID(s):
1812522 1563763
PAR ID:
10099212
Author(s) / Creator(s):
; ; ; ;
Date Published:
Journal Name:
Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI)
Page Range / eLocation ID:
323-338
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. End-to-end encrypted file-sharing systems enable users to share files without revealing the file contents to the storage servers. However, the servers still learn metadata, including user identities and access patterns. Prior work tried to remove such leakage but relied on strong assumptions. Metal (NDSS '20) is not secure against malicious servers. MCORAM (ASIACRYPT '20) provides confidentiality against malicious servers, but not integrity. Titanium is a metadata-hiding file-sharing system that offers confidentiality and integrity against malicious users and servers. Compared with MCORAM, which offers confidentiality against malicious servers, Titanium also offers integrity. Experiments show that Titanium is 5x-200x faster or more than MCORAM. 
    more » « less
  2. 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
  3. We consider the problems of data maintenance on untrusted clouds. Specifically, two important use cases: (i) using public-key encryption to enforce dynamic access control, and (ii) efficient key rotation. Enabling access revocation is key to enabling dynamic access control, and proxy re-encryption and related technologies have been advocated as tools that allow for revocation on untrusted clouds. Regrettably, the literature assumes that data is encrypted directly with the primitives. Yet, for efficiency reasons hybrid encryption is used, and such schemes are susceptible to key-scraping attacks. For key rotation, currently deployed schemes have insufficient security properties, or are computationally quite intensive. Proposed systems are either still susceptible to key-scraping attacks, or too inefficient to deploy. We propose a new notion of security that is practical for both problems. We show how to construct hybrid schemes that are both resistant to key-scraping attacks and highly efficient in revocation or key rotation. The number of modifications to the ciphertext scales linearly with the security parameter and logarithmically with the file length. 
    more » « less
  4. Industrial Control Systems (ICS) are the brain and backbone of nation's critical infrastructure such as nuclear power, water treatment, and petrochemical plants. In order to increase interoperability, real-time availability of data, and flexibility, information/communication technologies are adopted in this domain. While these information technologies have been effective, they are integrated into operational technologies without the necessary security defense. Designing an effective, layered security defense is not possible unless security threats are identified through a structural analysis of the ICS. For that reason, this paper provides an attacker's point of view on the reconnaissance effort necessary to gather details of the system dynamics - which are required for the development of sophisticated attacks. We present a reconnaissance approach which uses the system's I/O data to infer the dynamic model of the system. In this effort, we propose a novel cyber-attack which targets the controller proportional-integral-derivative gain values in a constant setpoint control system. Our findings will help researchers design more secure control systems. 
    more » « less
  5. Information flow tracking was proposed more than 40 years ago to address the limitations of access control mechanisms to guarantee the confidentiality and integrity of information flowing within a system, but has not yet been widely applied in practice for security solutions. Here, we survey and systematize literature on dynamic information flow tracking (DIFT) to discover challenges and opportunities to make it practical and effective for security solutions. We focus on common knowledge in the literature and lingering research gaps from two dimensions— (i) the layer of abstraction where DIFT is implemented (software, software/hardware, or hardware) and (ii) the security goal (confidentiality and/or integrity). We observe that two major limitations hinder the practical application of DIFT for on-the-fly security applications: (i) high implementation overhead and (ii) incomplete information flow tracking (low accuracy). We posit, after review of the literature, that addressing these major impedances via hardware parallelism can potentially unleash DIFT’s great potential for systems security, as it can allow security policies to be implemented in a built-in and standardized fashion. Furthermore, we provide recommendations for the next generation of practical and efficient DIFT systems with an eye towards hardware-supported implementations. 
    more » « less