Research Prompt: Capability-Based Instruction Safety Systems

Executive Summary

Investigate how different virtual machines, programming languages, operating systems, and effect systems handle instruction-level safety and capability control. Compare approaches to understand design trade-offs, implementation strategies, and theoretical foundations that could inform the Anoma Virtual Machine (AVM) instruction set architecture.

Research Questions

Primary Questions

How do modern virtual machines enforce instruction-level safety?
- What granularity of control do they provide?
- Is enforcement static (compile-time) or dynamic (runtime)?
- What is the performance impact of their approach?
How do effect systems track computational capabilities?
- How do they compose effects/capabilities?
- What type-system features enable capability tracking?
- How do they handle capability polymorphism?
How do capability-based operating systems manage resource access?
- What is the runtime model for capabilities?
- How do they handle capability delegation and revocation?
- What formal properties do they guarantee?
What are the theoretical foundations of capability systems?
- Object capabilities vs type-level capabilities
- Capability derivation and attenuation
- Formal verification approaches

Secondary Questions

How do different approaches handle composability?
- How do capabilities combine when composing programs?
- What algebraic properties do capability systems have?
- How do they handle capability conflicts?
What are the economic/resource aspects of capabilities?
- Can capabilities track computational cost (like EVM gas)?
- How do capability systems prevent resource exhaustion?
- Are there hybrid permission/economic models?
How do capability systems integrate with existing code?
- What are the migration paths from unsafe to capability-safe code?
- How do different capability regimes interoperate?
- What are the trusted computing base (TCB) implications?
What are the verification and formal methods aspects?
- What properties can be proven about capability systems?
- How do capability systems interact with theorem provers?
- What are the decidability/complexity trade-offs?

Domains to Investigate

1. Virtual Machines

Java Virtual Machine (JVM) - Java Security Manager and permission model - Stack inspection mechanism - Code signing and trust levels - SecurityManager API design - Performance impact of runtime checking - Migration from Security Manager (deprecated in Java 17)

Questions: - How does stack inspection work technically? - What are the performance benchmarks for permission checking? - Why was Security Manager deprecated? What replaced it? - How do permissions compose in hierarchical class loaders?

WebAssembly and WASI - WASI capability-based security model - Pre-opened directory capabilities - Capability passing at module instantiation - Sandboxing and isolation guarantees - Integration with host environments

Questions: - How are file descriptor capabilities represented? - What is the formal model of WASI capabilities? - How do WASI capabilities compare to POSIX permissions? - What are the portability implications?

Ethereum Virtual Machine (EVM) - Gas mechanism as implicit capability system - Gas costs for different operations - Gas metering and DoS prevention - Economic incentives in capability design - Storage vs computation costs

Questions: - How are gas costs determined and updated? - What is the relationship between gas and actual resource usage? - Could gas be used as a capability in non-economic contexts? - How does gas metering affect program optimization?

Other VMs to Consider: - CLR (.NET) Code Access Security (CAS) - now deprecated - Python restricted execution (also deprecated) - lessons learned - Lua sandboxing approaches - QuickJS security model - GraalVM polyglot sandboxing

2. Effect Systems and Programming Languages

Koka - Row polymorphism for effects - Effect inference and propagation - Effect handlers and semantics - Integration with linear types - Practical experience and case studies

Questions: - How is effect inference implemented? - What are the limits of effect polymorphism? - How do effect handlers compose? - Performance impact compared to untyped effects?

Frank - Effects as interfaces - Ability passing vs ambient effects - Effect pattern matching - Relationship to algebraic effects

Questions: - How does ability passing differ from Koka's approach? - What are the type-checking challenges? - How does Frank handle effect polymorphism?

Rust - Unsafe blocks and lexical scoping - Unsafe traits and implementations - Send/Sync as capability-like markers - Relationship to linear types - Minimal TCB design philosophy

Questions: - How is the unsafe boundary enforced? - What percentage of Rust code uses unsafe in practice? - How do Send/Sync interact with unsafe? - What are the verification challenges for unsafe code?

F* - Effect refinement types - Verification of effectful code - SMT integration for capability reasoning - Pre/post conditions for effects - Hybrid static/dynamic verification

Questions: - How are effects represented in the type system? - What can be automatically verified vs requires annotations? - How does F* handle effect polymorphism? - Scalability of verification approach?

OCaml Effects - Native algebraic effect support (5.0+) - Effect handlers implementation - Performance characteristics - Comparison with monadic effects

Questions: - How are effects implemented at runtime? - What are the performance benchmarks? - How do algebraic effects compose with modules?

Haskell - Monadic effect systems (mtl, transformers) - Effect libraries (polysemy, fused-effects, effectful) - IO and unsafePerformIO - RankNTypes for effect polymorphism

Questions: - How do different effect libraries compare? - What are the abstraction overhead costs? - How is unsafePerformIO controlled in practice?

Other Languages: - Scala 3 effect capabilities - Swift's async/await and actor isolation - Zig's comptime and runtime safety - Idris 2 dependent effects

3. Capability-Based Operating Systems

seL4 Microkernel - Formal verification of capability system - Capability derivation trees - Capability revocation algorithms - Performance characteristics - Real-world deployments

Questions: - How are capabilities represented in memory? - What is the verification proof strategy? - How does revocation scale? - What are the TCB size and complexity?

Capsicum (FreeBSD) - Capability mode semantics - Rights attenuation model - File descriptor capabilities - Integration with POSIX - Sandboxing strategies

Questions: - How does capability mode affect existing programs? - What are the adoption barriers? - How do capabilities compose with traditional permissions? - Performance overhead measurements?

KeyKOS/EROS/CapROS - Persistent capabilities - Orthogonal persistence model - Capability confinement - Historical lessons learned

Questions: - What are the advantages of persistent capabilities? - How does orthogonal persistence affect design? - Why didn't these systems achieve wider adoption?

Other Systems: - Genode OS framework - CloudABI capability-based API - Google Fuchsia capability routing - IBM System/38 object capabilities

4. Theoretical Foundations

Object Capability Model - Mark Miller's capability theory - Principle of least authority (POLA) - Confused deputy problem - Capability patterns (membrane, caretaker, etc.)

Questions: - What is the formal semantics of object capabilities? - How do object caps relate to type-level capabilities? - What properties are provable?

Algebraic Effect Theory - Plotkin and Pretnar's foundations - Effect handlers semantics - Free monad interpretation - Relationship to delimited continuations

Questions: - How do algebraic effects relate to capabilities? - What is the categorical semantics? - Can capability systems be modeled as algebraic theories?

Linear/Affine Type Theory - Resource tracking via linear types - Uniqueness types in Clean - Linear Haskell - Rust's affine types (move semantics)

Questions: - How do linear types enable capability control? - What is the relationship between linearity and capabilities? - Can we combine linear types with capability systems?

Formal Verification - Capability safety proofs - Information flow control - Noninterference properties - Verified compilation

Questions: - What properties of capability systems are verifiable? - How do we prove absence of capability leaks? - What are the proof automation strategies?

5. Database and Access Control Systems

PostgreSQL Row-Level Security - Policy-based access control - Role-based capabilities - Dynamic policy evaluation - Performance implications

Questions: - How are policies compiled and optimized? - What is the relationship to capability systems? - Can policies be statically analyzed?

Graph Databases and Traversal Permissions - Neo4j access control - RDF/SPARQL security - Path-based capabilities

Questions: - How do graph traversal permissions work? - Can capability systems model graph access patterns?

6. Distributed Systems

Macaroons (Google) - Decentralized authorization - Capability-like tokens - Attenuation and delegation - Cryptographic foundations

Questions: - How do macaroons differ from traditional capabilities? - What are the performance characteristics? - How do they handle revocation?

E Language - Distributed object capabilities - Promise-based capabilities - Capability-secure distributed computing

Questions: - How are capabilities transmitted across network? - What are the failure semantics? - How is capability integrity maintained?

Research Methodology

Literature Review

Primary Sources
- Original papers on capability systems (Dennis & Van Horn, 1966)
- Modern capability theory (Miller et al.)
- Effect system foundations (Plotkin, Pretnar, Leijen)
Implementation Studies
- Source code analysis of key systems
- Performance benchmarks and comparisons
- Case studies of real-world usage
Surveys and Comparisons
- Existing surveys of capability systems
- Effect system comparison papers
- Security analysis and threat models

Practical Investigation

Prototype Implementation
- Minimal capability system in Agda
- Comparison with current AVM design
- Performance and expressiveness evaluation
Case Studies
- Translate example programs across different capability models
- Measure expressiveness (lines of code, annotations needed)
- Identify common patterns and anti-patterns
Formal Analysis
- Prove properties about capability composition
- Verify no privilege escalation
- Compare proof complexity across models

Specific Topics to Deep Dive

Row Polymorphism for Capabilities

Koka's effect rows seem particularly promising for AVM. Investigate:

How row polymorphism works technically
Type inference with row constraints
Row unification algorithms
Extensible records and their relationship to effects
Subtyping with row types
Performance implications of row-based systems

Key Papers: - "Extensible Records with Scoped Labels" (Leijen, 2005) - "Koka: Programming with Row Polymorphic Effect Types" (Leijen, 2014) - "Type Directed Compilation of Row-Typed Algebraic Effects" (Leijen, 2017)

Economic Capabilities

EVM's gas system suggests combining permissions with resource tracking:

Cost models for different operations
Economic equilibria in capability systems
Preventing resource exhaustion attacks
Metering as a form of capability
Pricing strategies for computational resources

Key Papers: - "On the Economics of the Blockchain" (various authors on gas models) - "Resource-Aware Session Types" (combining resources with types) - "Capability-Based Financial Instruments" (Miller & Morningstar, 2000)

Verification of Capability Systems

Understanding what can be proven and how:

Capability safety definitions
Information flow theorems
Confinement properties
Automated verification tools
Proof strategies for capability preservation

Key Papers: - "Reasoning About Object Capabilities with a Kripke Logical Relation" (Swasey et al., 2017) - "Formal Verification of a Constant-Time Preserving C Compiler" (seL4-related) - "A Proof-Carrying File System" (capability-based FS verification)

Expected Outputs

1. Comparative Analysis Document

A comprehensive comparison table covering: - Granularity (coarse/fine-grained) - Enforcement timing (static/dynamic/hybrid) - Composability model (intersection/union/rows) - Performance characteristics - Formal properties guaranteed - TCB size and complexity - Practical adoption and lessons learned

2. Design Recommendations for AVM

Based on research, recommend: - Optimal capability granularity for AVM - Type system features to support capabilities - Composition mechanisms - Integration with existing Safety parameter - Migration strategy - Verification approach

3. Prototype Implementation

Working Agda code demonstrating: - Fine-grained capability system - Row polymorphism for capabilities (if beneficial) - Capability-safe program examples - Proofs of key safety properties - Performance analysis compared to current design

4. Research Paper Outline

Structure for potential publication: - Problem statement (instruction safety in VMs) - Survey of existing approaches - Novel contribution (AVM capability design) - Formal properties and proofs - Implementation and evaluation - Related work and comparison - Future directions

Timeline and Milestones

Phase 1: Literature Review (2-3 weeks) - Survey capability systems across domains - Identify key papers and implementations - Create annotated bibliography - Initial comparative analysis

Phase 2: Deep Dives (3-4 weeks) - Koka effect system detailed study - WASI capability model analysis - seL4 formal verification approach - EVM gas mechanics investigation - F* effect verification techniques

Phase 3: Prototype Design (2-3 weeks) - Design AVM capability system based on findings - Create formal specification - Prove key properties - Compare with current Safety parameter

Phase 4: Implementation (3-4 weeks) - Implement capability system in Agda - Create example programs - Performance evaluation - Integration testing

Phase 5: Documentation (2 weeks) - Write comprehensive comparison document - Create design recommendations - Prepare research paper outline - Documentation for AVM implementation

Resources and References

Books

"Capability-Based Computer Systems" (Henry M. Levy, 1984)
"Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control" (Mark S. Miller, 2006)
"Types and Programming Languages" (Pierce, 2002) - for type system foundations
"Advanced Topics in Types and Programming Languages" (Pierce, 2004) - effects chapter

Key Papers

Capability Systems: - Dennis & Van Horn, "Programming Semantics for Multiprogrammed Computations" (1966) - Miller et al., "Capability Myths Demolished" (2003) - Shapiro et al., "EROS: A Fast Capability System" (1999)

Effect Systems: - Plotkin & Pretnar, "Handling Algebraic Effects" (2013) - Leijen, "Koka: Programming with Row Polymorphic Effect Types" (2014) - Bauer & Pretnar, "Programming with Algebraic Effects and Handlers" (2015)

Verification: - Klein et al., "seL4: Formal Verification of an OS Kernel" (2009) - Swasey et al., "A Separation Logic for Fictional Sequential Consistency" (2015)

Virtual Machines: - Lindholm et al., "The Java Virtual Machine Specification" (various editions) - WebAssembly Specification, particularly WASI proposal

Online Resources

Koka Language: https://koka-lang.github.io/koka/doc/index.html
WASI Specification: https://github.com/WebAssembly/WASI
seL4 Documentation: https://sel4.systems/
Rust Unsafe Guidelines: https://rust-lang.github.io/unsafe-code-guidelines/
E Language and Capability Security: http://erights.org/

Tool and Systems to Experiment With

Koka compiler and examples
WebAssembly/WASI runtimes (wasmtime, wasmer)
F* verification tool
Agda development environment
Coq for capability proofs
Isabelle/HOL for seL4-style verification

Success Criteria

Research will be considered successful if it produces:

Comprehensive Understanding: Clear picture of capability system landscape
Actionable Recommendations: Concrete design decisions for AVM
Formal Foundation: Proofs of key safety properties
Working Prototype: Demonstrable capability-safe AVM programs
Publication Potential: Novel contributions to PL/security literature

Open Questions to Resolve

Priority questions that must be answered:

Should AVM use row polymorphism or fixed capability sets?
- Trade-off: Flexibility vs simplicity
- Investigate: Koka's experience, type inference complexity
Can capabilities track both permissions AND costs?
- Inspired by: EVM gas + traditional capabilities
- Investigate: Hybrid models, verification challenges
What is the minimal TCB for capability-safe AVM?
- Compare: seL4, Rust, WASI approaches
- Goal: Formally verified core
How to handle capability polymorphism in effect composition?
- Issue: Programs generic over capabilities
- Investigate: Effect polymorphism, subtyping
What migration path from current Safety parameter?
- Backward compatibility requirements
- Gradual typing analogy?

Collaboration and Expertise

Consult with experts in: - Effect systems: Daan Leijen (Koka), Ohad Kammar - Capability security: Mark S. Miller, Marc Stiegler - Formal verification: Gerwin Klein (seL4), Nikhil Swamy (F) - VM security: WebAssembly community, EVM researchers - Type theory:* PL theory community

Deliverables Checklist

Meta: How to Use This Prompt

This prompt can be used in several ways:

As a research assistant prompt: Feed to an AI research assistant for systematic investigation
As a graduate research project: Framework for MS/PhD thesis
As a grant proposal: Basis for research funding application
As a reading list: Structured guide for self-study
As a team task list: Distribute sections among research team

Recommended Approach: - Start with Phase 1 literature review - Identify 3-5 most promising approaches - Deep dive on those specific systems - Prototype hybrid design incorporating best ideas - Validate through formal proofs and implementation

This prompt was generated as part of AVM instruction safety design research. Last updated: 2025.