arXiv subjects

Hemant Gouni

Publications and source records attributed to Hemant Gouni.

3 recordsLinked to original sources

arXiv2026

The Duality of Information Flow: Reconciling Robust Downgrading with Non-Interference

Non-interference properties, spanning confidentiality and integrity, have long enjoyed a position as the high water mark of program security guarantees. Information flow type systems comprise the primary means for obtaining non-interference properties of programs, but their potential as a holy grail for secure programming has remained latent. Prior work bifurcates the type system along confidentiality and integrity, resulting in duplicate reasoning machinery and complex specifications. Furthermore, long-held wisdom dictates that non-interference must be weakened with downgrading mechanisms to accommodate the needs of practical programs, nearly all of which violate confidentiality and integrity in the course of fulfilling their purpose. This often pierces abstraction barriers and compromises modular reasoning. We introduce parametric information flow, which uses recent insights from modal type theory to shed light on these issues. In particular, we draw inspiration from work on the open and closed modalities, highlighting their rich interplay. Though each individual modality finds uses throughout the literature, our key insight is that their joint interaction suffices to reconstruct full-spectrum information flow reasoning, producing a single framework accounting for both confidentiality and integrity. Downgrading and analogues of advanced reasoning tools in the lineage of robust declassification are recovered without extensions to our theory, strengthening prior results. We show non-interference via a binary logical relations argument, realizing robustness as an ordinary 2-hyperproperty mediated by our modalities. Our work reveals state-of-the-art downgrading mechanisms to be wholly compatible with those for abstraction and modularity, arising precisely from the semantics of the latter under full-strength non-interference.

cs.PL↗

arXiv2024

Gradual C0: Symbolic Execution for Gradual Verification

Current static verification techniques support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on users. To solve this problem, prior work proposed gradual verification, which handles complete, partial, or missing specifications by soundly combining static and dynamic checking. Gradual verification has also been extended to programs that manipulate recursive, mutable data structures on the heap. Unfortunately, this extension does not reward users with decreased dynamic checking as specifications are refined. In fact, all properties are checked dynamically regardless of any static guarantees. Additionally, no full-fledged implementation of gradual verification exists so far, which prevents studying its performance and applicability in practice. We present Gradual C0, the first practicable gradual verifier for recursive heap data structures, which targets C0, a safe subset of C designed for education. Static verifiers supporting separation logic or implicit dynamic frames use symbolic execution for reasoning; so Gradual C0, which extends one such verifier, adopts symbolic execution at its core instead of the weakest liberal precondition approach used in prior work. Our approach addresses technical challenges related to symbolic execution with imprecise specifications, heap ownership, and branching in both program statements and specification formulas. We also deal with challenges related to minimizing insertion of dynamic checks and extensibility to other programming languages beyond C0. Finally, we provide the first empirical performance evaluation of a gradual verifier, and found that on average, Gradual C0 decreases run-time overhead between 11-34% compared to the fully-dynamic approach used in prior work. Further, the worst-case scenarios for performance are predictable and avoidable.

cs.LO↗

arXiv2022

Static Information Flow Control Made Simpler

Static information flow control (IFC) systems provide the ability to restrict data flows within a program, enabling vulnerable functionality or confidential data to be statically isolated from unsecured data or program logic. Despite the wide applicability of IFC as a mechanism for guaranteeing confidentiality and integrity -- the fundamental properties on which computer security relies -- existing IFC systems have seen little use, requiring users to reason about complicated mechanisms such as lattices of security labels and dual notions of confidentiality and integrity within these lattices. We propose a system that diverges significantly from previous work on information flow control, opting to reason directly about the data that programmers already work with. In doing so, we naturally and seamlessly combine the clasically separate notions of confidentiality and integrity into one unified framework, further simplifying reasoning. We motivate and showcase our work through two case studies on TLS private key management: one for Rocket, a popular Rust web framework, and another for Conduit, a server implementation for the Matrix messaging service written in Rust.

cs.PL↗