Symbolic abstract heaps for polymorphic information-flow guard inference

DOI10.1007/978-3-031-24950-1_4MaRDI QIDQ6132488zbMATH OpenOpenAlexFDO

Authors Nicolas Berthier, Narges Khakpour

Publication date 17 August 2023

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

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

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)

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.

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

Cites work

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

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)