SearcharxivSearch

arXiv subjects

Narges Khakpour

Publications and source records attributed to Narges Khakpour.

4 recordsLinked to original sources

VeriSBOM: Secure and Verifiable SBOM Sharing Via Zero-Knowledge Proofs

A Software Bill of Materials (SBOM) is a key component for the transparency of software supply chain; it is a structured inventory of the components, dependencies, and associated metadata of a software artifact. However, an SBOM often contain sensitive information that organizations are unwilling to disclose in full to anyone, for two main concerns: technological risks deriving from exposing proprietary dependencies or unpatched vulnerabilities, and business risks, deriving from exposing architectural strategies. Therefore, delivering a plaintext SBOM may result in the disruption of the intellectual property of a company. To address this, we present VeriSBOM, a trustless, selectively disclosed SBOM framework that provides cryptographic verifiability of SBOMs using zero-knowledge proofs. Within VeriSBOM, third parties can validate specific statements about a delivered software. Respectively, VeriSBOM allows independent third parties to verify if a software contains authentic dependencies distributed by official package managers and that the same dependencies satisfy rigorous policy constraints such as the absence of vulnerable dependencies or the adherence with specific licenses models. VeriSBOM leverages a scalable vector commitment scheme together with folding-based proof aggregation to produce succinct zero-knowledge proofs that attest to security and compliance properties while preserving confidentiality. Crucially, the verification process requires no trust in the SBOM publisher beyond the soundness of the underlying primitives, and third parties can independently check proofs against the public cryptographic commitments. We implement VeriSBOM, analyze its security, and evaluate its performance on real-world package registries. The results show that our method enables scalable, privacy-preserving, and verifiable SBOM sharing and validation.

cs.SE

Symmaries: Automatic Inference of Formal Security Summaries for Java Programs

We introduce a scalable, modular, and sound approach for automatically constructing formal security specifications for Java bytecode programs in the form of method summaries. A summary provides an abstract representation of a method's security behavior, consisting of the conditions under which the method can be securely invoked, together with specifications of information flows and aliasing updates. Such summaries can be consumed by static code analysis tools and also help developers understand the behavior of code segments, such as libraries, in order to evaluate their security implications when reused in applications. Our approach is implemented in a tool called Symmaries, which automates the generation of security summaries. We applied Symmaries to Java API libraries to extract their security specifications and to large real-world applications to evaluate its scalability. Our results show that the tool successfully scales to analyze applications with hundreds of thousands of lines of code, and that Symmaries achieves a promising precision depending on the heap model used. We prove the soundness of our approach in terms of guaranteeing termination-insensitive non-interference.

cs.CR

Symbolic Abstract Heaps for Polymorphic Information-flow Guard Inference (Extended Version)

In the realm of sound object-oriented program analyses for information-flow control, very few approaches adopt flow-sensitive abstractions of the heap that enable a precise modeling of implicit flows. To tackle this challenge, we advance a new symbolic abstraction approach for modeling the heap in Java-like programs. We use a store-less representation that is parameterized with a family of relations among references to offer various levels of precision based on user preferences. This enables us to automatically infer polymorphic information-flow guards for methods via a co-reachability analysis of a symbolic finite-state system. We instantiate the heap abstraction with three different families of relations. We prove the soundness of our approach and compare the precision and scalability obtained with each instantiated heap domain by using the IFSpec benchmarks and real-life applications.

cs.PL

Partially-Observable Security Games for Automating Attack-Defense Analysis

Network systems often contain vulnerabilities that remain unfixed in a network for various reasons, such as the lack of a patch or knowledge to fix them. With the presence of such residual vulnerabilities, the network administrator should properly react to the malicious activities or proactively prevent them, by applying suitable countermeasures that minimize the likelihood of an attack by the attacker. In this paper, we propose a stochastic game-theoretic approach for analyzing network security and synthesizing defense strategies to protect a network. To support analysis under partial observation, where some of the attacker's activities are unobservable or undetectable by the defender, we construct a one-sided partially observable security game and transform it into a perfect game for further analysis. We prove that this transformation is sound for a sub-class of security games and a subset of properties specified in the logic rPATL. We implement a prototype that fully automates our approach, and evaluate it by conducting experiments on a real-life network.

cs.CR