A Security Kernel Based on the Lambda-Calculus

Reference: Jonathan A. Rees (1996). MIT AI Laboratory Memo No. 1564. Source file: AIM-1564.pdf. URL

Summary

Rees describes Scheme 48, a programming environment whose design is guided by operating-system security principles. The security kernel is W7, a call-by-value lambda-calculus with extensions for abstract data types, object mutation, and hardware access. Each user or subsystem runs in a separate evaluation environment holding the objects representing that user’s privileges; because environments determine availability of object references, protection and sharing are controlled by construction.

The paper describes experience with Scheme 48 as the programming environment for Cornell’s mobile robots (no underlying OS) and as a secure multi-user workstation environment, arguing that lexical scope + first-class environments are a natural substrate for capability-style security among cooperating agents.

Key Ideas

Lambda-calculus as minimal security kernel via capability-style environments.
Scheme 48 (W7): modules, macros, dynamic isolation, portable across platforms.
Trust mediated by controlling which names bind to which objects.
Authentication via capsules (tamper-proof labelled objects).
Applied to robots and multi-user Scheme environments.

Connections

Conceptual Contribution

Claim: Lexical scope and first-class environments in a lambda-calculus variant (W7) are a sufficient security kernel: protection reduces to controlling which names bind to which object references.
Mechanism: Implements Scheme 48 as a capability-style environment where each user/subsystem runs in its own environment; authentication via capsules (tamper-proof labelled objects); deployed on Cornell mobile robots (no OS) and as multi-user workstation environment.
Concepts introduced/used: Capability Security, Lambda Calculus, Lexical Scope, Scheme 48, Capsules, Distributed Security, Multi-Agent Systems
Stance: foundational / engineering
Relates to: Provides a principled, capability-based alternative to the input-validation discipline of Seven Turrets Of Babel and the static DDoS analysis of A Language-Based Approach To Prevent DDoS; relevant to sandboxing malicious tools described in MalTool Malicious Tool Attacks.

Tags

#security #capabilities #lambda-calculus #foundational

Backlinks

Seven Turrets Of Babel line 27
Seven Turrets Of Babel line 20
index line 137
concept-map line 90
Scheme 48 line 6
Capsules line 6
Distributed Security line 11
A Language-Based Approach To Prevent DDoS line 27
A Language-Based Approach To Prevent DDoS line 19
Lexical Scope line 6
MalTool Malicious Tool Attacks line 28
Lambda Calculus line 6
Capability Security line 6

Linked Pages

MalTool Malicious Tool Attacks

MalTool: Malicious Tool Attacks on LLM Agents

Reference: Hu, Jia, Li, Song, Gong (2026). arXiv:2602.12194 (Duke, UC Berkeley). Source file: 2602.12194v2.pdf. URL

Summary

This paper presents the first systematic study of code-level malicious tool attacks on LLM agent ecosystems (MCP, Skills, mcp.so, skillsmp). Whereas prior work focused on crafting misleading tool names and descriptions, the authors show that genuinely harmful behaviour must be embedded in a tool’s implementation. They propose a CIA (confidentiality/integrity/availability) taxonomy of 12 concrete malicious behaviours (data exfiltration, credential abuse, data poisoning, file deletion, RCE downloading, CPU/GPU hijacking, DoS).

They build MalTool, a coding-LLM framework that iteratively synthesizes standalone and Trojan malicious tools using a behaviour-specific system prompt, diversity guidance, and an execution-based verifier. The result: 1,200 standalone malicious tools and 5,287 real-world tools with injected malicious behaviours. Detection methods (VirusTotal, Cisco MCP Scanner, MCPScan) perform poorly, motivating new defences.

Key Ideas

CIA taxonomy of malicious tool behaviours in agent settings.
Automatic generation pipeline: system prompt + coding LLM + execution-based verifier.
Trojan construction by embedding malicious logic in benign tool code.
Existing malware and MCP-specific scanners fail on both false-positives and false-negatives.
Dataset released for benign tools only to minimize misuse.

Connections

Conceptual Contribution

Claim: Truly harmful behaviour in LLM Agents ecosystems lives in tool implementations, not in their descriptions; prior description-level red-teaming misses the dominant attack class, and current scanners miss it too.
Mechanism: Introduces a CIA taxonomy of 12 malicious behaviours; builds MalTool, a coding-LLM pipeline (behaviour-specific system prompt + diversity guidance + execution-based verifier) that produces standalone and Trojan tools; benchmarks VirusTotal, Cisco MCP Scanner, MCPScan and shows poor detection.
Concepts introduced/used: Tool Use, Model Context Protocol, Trojan Tools, Prompt Injection, Agent Security, LLM Agents, Distributed Security
Stance: empirical
Relates to: Deepens the tool/MCP threat surface catalogued in AI Agents Under Threat and Survey Of Agent Interoperability Protocols; motivates language-based defences akin to A Language-Based Approach To Prevent DDoS and capability isolation of Security Kernel Lambda Calculus.

Tags

A Language-Based Approach To Prevent DDoS

A Language-Based Approach to Prevent DDoS Attacks in Distributed Financial Agent Systems

Reference: Fazeldehkordi, Owe, Ramezanifarkhani (2018). University of Oslo. Source file: A language-based approach to prevent DDoS attacks in distributed financial agent systems.pdf. URL

Summary

The authors propose adding a language-based layer of defense against DoS/DDoS to distributed financial agent systems built on the actor model with asynchronous method calls and futures (in the style of Creol/ABS). Because such languages make it cheap to launch non-blocking floods, they adapt a static analysis for detecting call-flooding cycles to the many-to-one DDoS setting.

The analysis builds per-method control-flow graphs, identifies cycles, and classifies nodes as strongly- or weakly-reachable to detect unbounded method-call generation at compile time. They distinguish one-to-one, many-to-one, and one-to-many flooding, and illustrate with a publish/subscribe newsletter example where future-based optimization accidentally enables a DoS against subscribers.

Key Ideas

Static detection of call-based flooding in actor-model languages with futures.
Classification: one-to-one, many-to-one, one-to-many flooding.
Strong vs weak reachability in control-flow cycles.
Instantiation flooding (unbounded object creation) as a resource-exhaustion vector.
Application to financial service subscriber systems.

Connections

Conceptual Contribution

Claim: Actor-based agent languages with asynchronous futures make DoS/DDoS cheap to launch inadvertently, and static analysis of call-flow cycles can prevent it at compile time.
Mechanism: Builds per-method control-flow graphs, detects strongly/weakly-reachable cycles that generate unbounded calls; extends from one-to-one to many-to-one and one-to-many flooding; illustrated on a Creol/ABS publish/subscribe newsletter.
Concepts introduced/used: Static Analysis, Actor Model, Futures, DDoS, Control-Flow Graph, Distributed Security, Multi-Agent Systems
Stance: engineering
Relates to: Shares the language-level-security stance of Seven Turrets Of Babel and Security Kernel Lambda Calculus; addresses a threat class complementary to the tool-level attacks of MalTool Malicious Tool Attacks and the broad landscape of AI Agents Under Threat.

Tags

Seven Turrets Of Babel

The Seven Turrets of Babel: A Taxonomy of LangSec Errors and How to Expunge Them

Reference: Momot, Bratus, Hallberg, Patterson (2016). IEEE Cybersecurity Development (SecDev). Source file: 7turretsaspublished.pdf. URL

Summary

The authors catalogue seven recurring classes of input-handling bugs under the LangSec (language-theoretic security) lens: shotgun parsing, non-minimalist input-handling code, differing interpretations of the input language, incomplete protocol specification, overloaded fields in input format, permissive processing of invalid input, and inability to express input languages in the Chomsky hierarchy. Each class is grounded in concrete CVEs (Heartbleed, Android Master Key, Rosetta Flash, OpenSSL CVE-2016-0752).

LangSec’s remedy is to treat input acceptance as a formal language-recognition problem: specify a grammar no more complex than deterministic context-free, build a recognizer that fully validates before any processing, and cleanly separate parsing from application logic. The paper proposes new CWE entries naming each weakness so auditors can precisely describe vulnerable input-handling code.

Key Ideas

LangSec: input should be a well-defined language with a fully-validating recognizer.
Seven anti-patterns: shotgun parsing, non-minimalist code, interpretation drift, incomplete spec, field overloading, permissive invalid input, undecidable grammars.
Chomsky hierarchy as a safety ceiling for input languages.
Hand-rolled parsers vs parser-combinator / generator tooling (e.g., Hammer).
Proposed new CWEs to label LangSec anti-patterns.

Connections

Conceptual Contribution

Claim: Most serious input-handling vulnerabilities reduce to seven recurring anti-patterns, all addressable by treating input acceptance as a formal language-recognition problem bounded by the Chomsky hierarchy.
Mechanism: Catalogues each anti-pattern (shotgun parsing, non-minimalist code, interpretation drift, incomplete spec, field overloading, permissive invalid input, undecidable grammars) against real CVEs (Heartbleed, Android Master Key, Rosetta Flash); prescribes grammar-first validating recognizers and proposes new CWE entries.
Concepts introduced/used: LangSec, Shotgun Parsing, Chomsky Hierarchy, Parser Combinators, Distributed Security, Common Weakness Enumeration
Stance: engineering / critique
Relates to: Shares a language-theoretic security stance with A Language-Based Approach To Prevent DDoS and Security Kernel Lambda Calculus; its grammar-discipline arguments apply directly to the schema/protocol surfaces catalogued in Survey Of Agent Interoperability Protocols and exploited in MalTool Malicious Tool Attacks.

Tags

Multi-Agent Systems

Multi-Agent Systems

Systems of multiple autonomous agents that interact, coordinate, and sometimes compete.

Foundations

Intelligent Agents Theory and Practice — Wooldridge
Multiagent Systems Sycara
Agent-Oriented Programming — Shoham

Coordination & robustness

See also

Distributed Security

Distributed Security

Security of distributed/agent systems: mobile code, secure messaging, language-based defences.

Related

Capsules

Encapsulated units of code and authority that can be passed between principals without exposing their internals. In the security-kernel lambda calculus, capsules are the primitive bearers of capability-style authority, providing a semantic basis for object-capability security.

In this vault

Scheme 48

A byte-coded implementation of the Scheme programming language designed with a small, auditable core and module system. Used as a substrate for research on security kernels and capability-based systems.

In this vault

Security Kernel Lambda Calculus

Lexical Scope

The binding rule in which a name’s referent is determined by its textual surroundings at definition time, providing the closure discipline that underpins capability-based security in lambda-calculus-style kernels.

In this vault

Lambda Calculus

Lambda Calculus

A formal system introduced by Church that expresses computation via function abstraction and application. It serves as a foundational model of computation and the theoretical basis for functional programming languages.

In this vault

Security Kernel Lambda Calculus

Capability Security

Capability Security

Access-control style where authority is conveyed by unforgeable object references; lexical scope in languages like Scheme suffices as a capability kernel.

In this vault