Symmaries: Automatic Inference of Formal Security Summaries for Java Programs

• URL: http://arxiv.org/abs/2512.20396v1
• Date: Tue, 23 Dec 2025 14:33:31 GMT
• Title: Symmaries: Automatic Inference of Formal Security Summaries for Java Programs
• Authors: Narges Khakpour, Nicolas Berthier,
• Abstract summary: We introduce a scalable, modular, and sound approach for constructing formal security specifications for Java bytecode programs.<n>A summary provides an abstract representation of a method's security behavior.<n>Our approach is implemented in a tool called Symmaries, which automates the generation of security summaries.
• Score: 0.7305019142196582
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• From Detection to Prevention: Explaining Security-Critical Code to Avoid Vulnerabilities [2.490168997159702]
  This work explores a proactive strategy to prevent vulnerabilities by highlighting code regions that implement security-critical functionality.<n>We present an IntelliJ IDEA plugin prototype that uses code-level software metrics to identify potentially security-critical methods.
  arXiv  Detail & Related papers  (2026-01-31T13:16:01Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• Rethinking Testing for LLM Applications: Characteristics, Challenges, and a Lightweight Interaction Protocol [83.83217247686402]
  Large Language Models (LLMs) have evolved from simple text generators into complex software systems that integrate retrieval augmentation, tool invocation, and multi-turn interactions.<n>Their inherent non-determinism, dynamism, and context dependence pose fundamental challenges for quality assurance.<n>This paper decomposes LLM applications into a three-layer architecture: textbftextitSystem Shell Layer, textbftextitPrompt Orchestration Layer, and textbftextitLLM Inference Core.
  arXiv  Detail & Related papers  (2025-08-28T13:00:28Z)
• Exposing Go's Hidden Bugs: A Novel Concolic Framework [2.676686591720132]
  We present Zorya, a novel methodology to evaluate Go programs comprehensively.<n>By systematically exploring execution paths to uncover vulnerabilities beyond conventional testing, symbolic execution offers distinct advantages.<n>Our solution employs Ghidra's P-Code as an intermediate representation (IR)
  arXiv  Detail & Related papers  (2025-05-26T16:26:20Z)
• MARVEL: Multi-Agent RTL Vulnerability Extraction using Large Language Models [15.35860248847857]
  Large Language Models (LLMs) have been used to assist during this task, either directly or in conjunction with existing tools.<n>We propose MARVEL, a multi-agent LLM framework for a unified approach to decision-making, tool use, and reasoning.
  arXiv  Detail & Related papers  (2025-05-17T11:31:24Z)
• Secure Synthesis of Distributed Cryptographic Applications (Technical Report) [1.9707603524984119]
  We advocate using secure program partitioning to synthesize cryptographic applications. This approach is promising, but formal results for the security of such compilers are limited in scope. We develop a compiler security proof that handles subtleties essential for robust, efficient applications.
  arXiv  Detail & Related papers  (2024-01-06T02:57:44Z)
• The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verification [3.2925005312612323]
  This paper presents the FormAI dataset, a large collection of 112, 000 AI-generated C programs with vulnerability classification. Every program is labeled with the vulnerabilities found within the source code, indicating the type, line number, and vulnerable function name. We make the source code available for the 112, 000 programs, accompanied by a separate file containing the vulnerabilities detected in each program.
  arXiv  Detail & Related papers  (2023-07-05T10:39:58Z)
• CodeLMSec Benchmark: Systematically Evaluating and Finding Security Vulnerabilities in Black-Box Code Language Models [58.27254444280376]
  Large language models (LLMs) for automatic code generation have achieved breakthroughs in several programming tasks. Training data for these models is usually collected from the Internet (e.g., from open-source repositories) and is likely to contain faults and security vulnerabilities. This unsanitized training data can cause the language models to learn these vulnerabilities and propagate them during the code generation procedure.
  arXiv  Detail & Related papers  (2023-02-08T11:54:07Z)
• Realistic simulation of users for IT systems in cyber ranges [63.20765930558542]
  We instrument each machine by means of an external agent to generate user activity. This agent combines both deterministic and deep learning based methods to adapt to different environment. We also propose conditional text generation models to facilitate the creation of conversations and documents.
  arXiv  Detail & Related papers  (2021-11-23T10:53:29Z)
• Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
  We present a Symbolic Reinforcement Learning (SRL) based architecture for safety control of Radio Access Network (RAN) applications. We provide a purely automated procedure in which a user can specify high-level logical safety specifications for a given cellular network topology. We introduce a user interface (UI) developed to help a user set intent specifications to the system, and inspect the difference in agent proposed actions.
  arXiv  Detail & Related papers  (2021-06-03T16:45:40Z)
• An Abstraction-based Method to Verify Multi-Agent Deep Reinforcement-Learning Behaviours [8.95294551927446]
  Multi-agent reinforcement learning (RL) often struggles to ensure the safe behaviours of the learning agents. We present a methodology that combines formal verification with (deep) RL algorithms to guarantee the satisfaction of formally-specified safety constraints.
  arXiv  Detail & Related papers  (2021-02-02T11:12:30Z)
• Evaluating the Safety of Deep Reinforcement Learning Models using Semi-Formal Verification [81.32981236437395]
  We present a semi-formal verification approach for decision-making tasks based on interval analysis. Our method obtains comparable results over standard benchmarks with respect to formal verifiers. Our approach allows to efficiently evaluate safety properties for decision-making models in practical applications.
  arXiv  Detail & Related papers  (2020-10-19T11:18:06Z)
• SAMBA: Safe Model-Based & Active Reinforcement Learning [59.01424351231993]
  SAMBA is a framework for safe reinforcement learning that combines aspects from probabilistic modelling, information theory, and statistics. We evaluate our algorithm on a variety of safe dynamical system benchmarks involving both low and high-dimensional state representations. We provide intuition as to the effectiveness of the framework by a detailed analysis of our active metrics and safety constraints.
  arXiv  Detail & Related papers  (2020-06-12T10:40:46Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.