Type-based information flow analysis for $π$-calculus with a dynamically extensible security lattice

• URL: http://arxiv.org/abs/2606.27059v1
• Date: Thu, 25 Jun 2026 14:03:51 GMT
• Title: Type-based information flow analysis for $π$-calculus with a dynamically extensible security lattice
• Abstract summary: We develop a type system for secure information flow where new security levels can be inserted into the security lattice dynamically.<n>Our system is formalized by extending Kobayashi's type-based secure information flow analysis for Milner's pi-calculus.
• Score: 0.0
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: We develop a type system for secure information flow where new security levels can be created and inserted into the security lattice dynamically, i.e., even in the middle of an execution of a system. Our system is formalized by extending Kobayashi's type-based secure information flow analysis for Milner's pi-calculus, which is one of the most expressive models (or "languages") supporting both sequential and concurrent computations, with concise syntax, reduction-based semantics, and bisimulation equivalence as a robust formalization of secrecy as non-interference. The development required careful treatment of extensions of lattices themselves as well as deliberate generalization from the simple 2-element lattice (consisting of only High and Low) in the original system.

Related papers

• Provably Secure Agent Guardrail [89.79561918065122]
  Existing defense architectures rely on empirical semantic guardrails and probabilistic large model adjudicators.<n>This paper proposes a new security paradigm for agents based on the fundamental limitations of logical reasoning.
  arXiv  Detail & Related papers  (2026-05-28T02:12:41Z)
• HIPO: Instruction Hierarchy via Constrained Reinforcement Learning [57.40686733111483]
  textscHIPO is a novel alignment framework that formulates HIF as a Constrained Markov Decision Process.<n>textscHIPO elevates system prompts from mere input context to strict algorithmic boundaries.
  arXiv  Detail & Related papers  (2026-03-17T06:12:41Z)
• Just Ask: Curious Code Agents Reveal System Prompts in Frontier LLMs [65.6660735371212]
  We present textbftextscJustAsk, a framework that autonomously discovers effective extraction strategies through interaction alone.<n>It formulates extraction as an online exploration problem, using Upper Confidence Bound--based strategy selection and a hierarchical skill space spanning atomic probes and high-level orchestration.<n>Our results expose system prompts as a critical yet largely unprotected attack surface in modern agent systems.
  arXiv  Detail & Related papers  (2026-01-29T03:53:25Z)
• Kernel-Based Learning of Safety Barriers [0.9367224590861915]
  Rapid integration of AI algorithms in safety-critical applications is raising concerns about the ability to meet stringent safety standards.<n>Traditional tools for formal safety verification struggle with the black-box nature of AI-driven systems.<n>We present a data-driven approach for safety verification and synthesis of black-box systems with discrete-time dynamics.
  arXiv  Detail & Related papers  (2026-01-17T10:42:35Z)
• LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems [0.8574682463936006]
  Traditional formal verification tools fall short when faced with systems that embed both opaque black-box AI components and complex dynamics.<n>We introduce LUCID, a verification engine for certifying safety of black-box embedding dynamical systems.<n> LUCID is the first known tool capable of establishing quantified safety guarantees for such systems.
  arXiv  Detail & Related papers  (2025-12-12T17:46:50Z)
• Rule Encoding and Compliance in Large Language Models: An Information-Theoretic Analysis [0.0]
  The design of safety-critical agents based on large language models (LLMs) requires more than simple prompt engineering.<n>This paper presents a comprehensive information-theoretic analysis of how rule encodings in system prompts influence attention mechanisms and compliance behaviour.
  arXiv  Detail & Related papers  (2025-09-23T14:42:32Z)
• The Alignment Trap: Complexity Barriers [0.0]
  This paper argues that AI alignment is not merely difficult, but is founded on a fundamental logical contradiction.<n>We first establish Theion Paradox: we use machine learning precisely because we cannot enumerate all necessary safety rules.<n>This paradox is then confirmed by a set of five independent mathematical proofs.
  arXiv  Detail & Related papers  (2025-06-12T02:30:30Z)
• Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation [52.626086874715284]
  We introduce a novel problem formulation called Abstract DNN-Verification, which verifies a hierarchical structure of unsafe outputs.<n>By leveraging abstract interpretation and reasoning about output reachable sets, our approach enables assessing multiple safety levels during the formal verification process.<n>Our contributions include a theoretical exploration of the relationship between our novel abstract safety formulation and existing approaches.
  arXiv  Detail & Related papers  (2025-05-08T13:29:46Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
  arXiv  Detail & Related papers  (2024-03-15T17:32:02Z)
• Decrypting Nonlinearity: Koopman Interpretation and Analysis of Cryptosystems [0.05120567378386613]
  We introduce a novel perspective on cryptosystems by viewing the Diffie-Hellman key exchange and the Rivest-Shamir-Adleman cryptosystem as nonlinear dynamical systems.<n>By applying Koopman theory, we transform these dynamical systems into higher-dimensional spaces and analytically derive equivalent purely linear systems.
  arXiv  Detail & Related papers  (2023-11-21T16:38:48Z)
• Iterative Sketching for Secure Coded Regression [66.53950020718021]
  We propose methods for speeding up distributed linear regression. Specifically, we randomly rotate the basis of the system of equations and then subsample blocks, to simultaneously secure the information and reduce the dimension of the regression problem.
  arXiv  Detail & Related papers  (2023-08-08T11:10:42Z)
• Perfectly Secure Steganography Using Minimum Entropy Coupling [60.154855689780796]
  We show that a steganography procedure is perfectly secure under Cachin 1998's information-theoretic model of steganography. We also show that, among perfectly secure procedures, a procedure maximizes information throughput if and only if it is induced by a minimum entropy coupling.
  arXiv  Detail & Related papers  (2022-10-24T17:40:07Z)

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.