Symbolic abstract heaps for polymorphic information-flow guard inference

DOI10.1007/978-3-031-24950-1_4zbMATH Open1529.68079arXiv2211.03450OpenAlexW4316662773MaRDI QIDQ6132488FDOQ6132488

Authors: Nicolas Berthier, Narges Khakpour 

Publication date: 17 August 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/2211.03450

Recommendations

• Exact heap summaries for symbolic execution
• Abstract Interpretation of Symbolic Execution with Explicit State Updates
• Static Analysis
• A sound analysis for secure information flow using abstract memory graphs
• Verification, Model Checking, and Abstract Interpretation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Cites Work

• Graph-Based Algorithms for Boolean Function Manipulation
• Secure Information Flow as a Safety Property
• Title not available (Why is that?)
• Information flow inference for ML
• Monotone data flow analysis frameworks
• Secure information flow by self-composition
• Abstract non-interference
• A logic for information flow in object-oriented programs
• Certification of programs for secure information flow
• Precise interprocedural dataflow analysis with applications to constant propagation
• A Certified Lightweight Non-interference Java Bytecode Verifier
• Static Analysis
• A security flow control algorithm and its denotational semantics correctness proof
• Title not available (Why is that?)

This page was built for publication: Symbolic abstract heaps for polymorphic information-flow guard inference

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6132488)