Security Domain Specific Languages (DSLs) bring structure and and tractable reasoning to security properties of systems. The power of Security DSLs can introduce assurance at the level of Automated Reasoning (AR) to unverified systems without requiring developers to adopt tools like formal methods. In other words, Security DSLs can make high-assurance development accessible to developers without the capacity to apply AR themselves. However, taking advantage of the full power of Security DSLs still requires security experts who understand the context that their systems operate in. In this talk, I will show how we can apply AR techniques to automatically and on-demand infer the context that systems operate in to generate Security DSL programs to automatically evaluate security and compliance properties. Combining Security DSLs and AR creates a flywheel that lets us assess the security of systems more quickly and comprehensively than is possible with either alone.
Tristan Ravitch isa Principal Applied Scientist at Amazon Web Services
Verified programs are often developed in high-level, safe environments, but they must ultimately run in low-level systems languages, where maintaining their intended invariants becomes challenging. We present Crane, an alternative extraction approach from the Rocq Prover to production-grade modern C++ for large-scale systems. Crane generates functional C++ with disciplined use of memory- and thread-safe abstractions and supports mappings from Rocq data types to both C++ standard library types and Bloomberg internal libraries. Many Rocq developments define structured input languages together with verified recognizers and transformations; Crane enables extracting these components into C++, making it practical to deploy formally verified parsers and validators in production systems. We also provide concurrency primitives that compile to safe C++ abstractions for composable concurrent execution, and use AI agents to accelerate Crane's development and auto-formalization of verified libraries. This talk outlines the design, implementation challenges, and early lessons learned in integrating verified programs into real-world C++ systems.
Felix 'FX' Lindner, a visionary computer security researcher who helped to shape a generation of hackers and security reseeachers and brought together hackers and academics, passed away this year. FX was an early champion and practitioner of LangSec, and gave the concluding keynote of the first LangSec workshop. We will remember Felix's contributions in a brief note from the workshop organizers.
Large Language Models (LLMs) have become ubiquitous in program proof generation. Before a proof can be generated, software specifications must be provided to formally describe the programmer's intent when developing the software. Writing program specifications then become the bottleneck in large-scale program proving. We report on our preliminary experiments on several million lines of open source components. Obtaining high accuracy relies on the introduction of validity oracles to ensure that inferred specifications are valid. We discuss different levels of specification validity based on a family of oracles employed on the output of the LLM, providing the basis for automated specification inference and repair for large C++ programs. We discuss what is next to come for automated program verification using LLMs and address potential threats to validity, such as the risk of a circular dependence in generating specifications from code itself.
Julien Vanegue is the head of infrastructure and security research in the office of the CTO at Bloomberg in New York, USA
In the seventy years since the Chomsky Hierarchy, the practice of writing and reasoning about code to recognize and parse inputs to computing system has given rise to far more language classes than a student encounters in a Sipser-based theory course. In this paper, we seek to systematize some of these classes with the context of each other into a larger hierarchy, as well as to define the most general forms of currently open questions on parsing complexity. We also look at some real-world data formats and protocols and categorize where they fall (or could fall) in the new expanded hierarchy.
The formal language theory led to groundbreaking theoretical results on the decidability of many problems, often proven with algorithms with intractable worst-case complexity. This article focuses on the efficient computation of the intersection between context-free and regular languages, which can be highly interesting for source code static analysis. We propose two new faster algorithms: (1) a general-purpose algorithm for fast intersection based on heuristics and (2) an asymptotically optimal algorithm named JUNID (for "Junction Identification") for intersection with incomplete sentences, which is especially important for statically detecting injection vulnerabilities. An experimental study supports our claims. The implementations of the algorithms and the proofs verified with the Coq proof assistant are available to the reader.
Contemporary multi-agent communication protocols face a fundamental tension: extensibility requires expressive power, but expressive power creates unbounded attack surfaces. We present CBCL (Common Business Communication Language), an agent communication language that resolves this tension by constraining all messages, including runtime language extensions, to the deterministic context-free language (DCFL) class. CBCL allows agents to define, transmit, and adopt domain-specific "dialect" extensions as first-class messages; three safety invariants (R1–R3) are machine-checked for dialect definitions in Lean 4 and enforced in a GNU Guile reference implementation, preventing unbounded expansion, applying declared resource limits, and preserving core vocabulary. We formalize the language and its safety properties in Lean 4, implement a reference parser and dialect engine in GNU Guile Scheme (25 test files), and extract a verified parser binary. Our results demonstrate that homoiconic protocol design, where extension definitions share the same representation as ordinary messages, can be made provably safe. As autonomous agents increasingly act, negotiate, and extend their own capabilities, formally constraining what they can express to each other is a necessary condition for enforcing human intent.
Language-theoretic security requires systems to fully recognize untrusted input before processing it, but comprehensive validation at every function boundary introduces overhead that deters adoption. This paper reduces that overhead by presenting provenance-aware parse insertion, a static analysis technique that computes minimal locations for parser placement by tracking parameter modification status across interprocedural boundaries. Our key insight is that pass-through parameters, those unchanged within a function, inherit their validation status from callers and do not need to be re-validated in callees. Only modified parameters that represent new values require new validation. We formalize this as a two-phase analysis: intraprocedural def-use analysis computes function summaries that record parameter modifications, while interprocedural propagation tracks taint validation levels across the call graph, respecting pass-through semantics. We discuss our implementation of this toolkit and evaluate its performance on two open-source targets. The source code of the analyzer will be available.
Language-theoretic security argues that software handling untrusted input should treat that input as a formal language and implement a recognizer whose behavior matches the intended specification. In low-level systems code, however, many security-critical interfaces are not exposed as obvious parsers. Instead, they accept streams of buffers, calls, flags, object references, and state-dependent operations whose effective input language is implicit in implementation behavior. This gap makes it difficult to determine what inputs are truly recognized, what state transitions are permitted, and where malformed or adversarial sequences are accepted in practice. We present an object-centric tracing approach for language-theoretic security analysis of low-level interfaces. Our method reconstructs execution around objects, lifetimes, and state transitions rather than around raw instructions or isolated events. By treating interface interactions as traces over object states and operations, we derive empirical models of the interface’s accepted language and identify deviations between expected and observed behavior. These deviations surface as anomalous transition sequences, inconsistent object-state evolution, lifetime violations, and parser-like over-acceptance at interface boundaries. We demonstrate how object-centric tracing helps analyze security-relevant low-level behaviors that are difficult to capture with conventional tracing alone, including multi-step misuse patterns that precede memory corruption and state confusion. Across case studies, we show that object-centric trace views make it possible to reason about low-level interfaces in language-theoretic terms: what symbols are consumed, what state machine is actually implemented, and where the implementation admits unsafe strings in the language. Our results suggest that object-centric tracing can serve as a practical bridge between principles and real-world low-level security analysis.
Python's native serialization protocol, pickle, is a powerful but insecure format for transferring untrusted data. It is frequently used, especially for saving machine learning models, despite the known security challenges. While developers sometimes mitigate this risk by restricting imports during unpickling or using static and dynamic analysis tools, these approaches are error-prone and depend heavily on accurate interpretations of the Pickle Virtual Machine (PVM) opcodes. Discrepancies across Python's three native PVM modules---pickle (Python), _pickle (C), and pickletools (Python disassembler)---can lead to incorrect detection of malicious payloads and undermine existing defenses. To efficiently and scalably identify discrepancies, we present PICKLEFUZZER, a custom generation-based fuzzer that identifies inconsistencies across pickle implementations. PICKLEFUZZER generates pickle objects, passes them to each implementation, and detects differences in thrown exceptions or changes to key internal states. PICKLEFUZZER generates pickle objects using a grammar, which we developed to account for the missing pickle specification. PICKLEFUZZER determines discrepancies by comparing the execution behaviors of each test implementation, rather than requiring a specification-derived oracle. PICKLEFUZZER successfully detected 14 new discrepancies in the pickle implementation. Four discrepancies are critical and can be used to bypass security-critical scanning tools like those deployed on the popular model hosting platform, Hugging Face. We disclosed all findings to the Python Software Foundation for remediation, and additionally disclosed the security issues to a bug bounty platform and were awarded a $750 bounty. We demonstrate that differential testing is a viable approach for identifying security-relevant discrepancies in important pickle implementations, and our work can lead to promising future directions for finding deeper pickle bugs with more directed fuzzing.
As AI is expanding into the domain of formal methods (e.g., [1, 2]), we must ask: Can AI help LangSec? Can LangSec help AI? And if so, what might be the special connections between LangSec, AI, and emergent execution/weird machines?