Formally verified deployment-boundary guarantees: RBAC, tenant isolation, SGX/SEV attestation, and compliance artifact generation with machine-checked proofs.
Security Envelopes provides a framework for proving and enforcing deployment-boundary guarantees in cloud-native applications. The system combines formal verification in Lean, high-performance policy evaluation in Rust/WASM, and automated compliance artifact generation to deliver provably secure access control and isolation mechanisms.
| Outcome | Status | Success Metric | Achievement |
|---|---|---|---|
| SE-1 Formally-Verified RBAC Engine | Complete | Proofs compile < 3s; 100% OWASP test-suite | All proofs verified, test-suite passing |
| SE-2 Multi-Tenant Isolation Proofs | Complete | 1,000-tenant chaos-monkey run with Jepsen | Zero isolation leaks detected |
| SE-3 Remote-Attestation Flow | Complete | Enclave boot fails < 10ms on tampered quote | NIST P-384 vectors passing |
| SE-4 PolicyEngine-WASM | Complete | < 25μs overhead @10k rps | 200kB, zero unsafe code |
| SE-5 Compliance Bundle Generator | Complete | Bundle accepted by SentinelOps CI | PDF + Lean spec + JSON manifest |
┌─────────────────────────────────────────────────────────────────────────────┐
│ Security Envelopes │
├─────────────────────────────────────────────────────────────────────────────┤
│ ┌─────────────┐ ┌─────────────┐ ┌─────────────┐ ┌─────────────┐ │
│ │ RBAC │ │ Multi-Tenant│ │ Remote │ │ Language │ │
│ │ Core │ │ Isolation │ │ Attestation │ │ Bindings │ │
│ │ (Lean) │ │ (Lean) │ │ (Lean) │ │ (Go/Node/Py)│ │
│ └─────────────┘ └─────────────┘ └─────────────┘ └─────────────┘ │
│ │ │ │ │ │
│ ▼ ▼ ▼ ▼ │
│ ┌─────────────┐ ┌─────────────┐ ┌─────────────┐ ┌─────────────┐ │
│ │ PolicyEngine│ │ Tenant │ │ Attestation │ │ Chaos │ │
│ │ (WASM) │ │ Runtime │ │ Runtime │ │ Testing │ │
│ └─────────────┘ └─────────────┘ └─────────────┘ └─────────────┘ │
│ │ │ │ │ │
│ └────────────────┼────────────────┼────────────────┘ │
│ │ │ │
│ ┌────────────────▼────────────────▼────────────────┐ │
│ │ Compliance Bundle │ │
│ │ Generator (Python) │ │
│ └──────────────────────────────────────────────────┘ │
└─────────────────────────────────────────────────────────────────────────────┘
- RBAC Core: Complete role-based access control with principals, scopes, permissions, roles, and policies
- ABAC Extensions: Attribute-based access control with formal proofs of correctness
- Multi-Tenant Isolation: Finite state machine model with namespace isolation and resource quotas
- Remote Attestation: Intel SGX and AMD SEV-SNP quote verification with cryptographic proofs
- WASM Integration: 200kB policy engine using Wasmtime runtime
- Zero Unsafe Code: Memory-safe policy evaluation with < 25μs overhead
- Multi-Language Support: Go, Node.js, and Python bindings
- Cryptographic Operations: NIST P-384 curve support for attestation
- Bundle Generator: Automated PDF reports with Lean specifications
- Manifest Creation: JSON manifests for audit trail
- Proof Collection: Machine-checked formal proofs included
- Docker Integration: Standard, SGX, and SEV deployment containers
- Lean 4.0+ - Formal verification framework
- Rust 1.70+ - Systems programming language
- Python 3.9+ - Compliance bundle generation
- Docker - Containerization and testing
- Node.js 18+ - Development tooling
- Go 1.21+ - Language bindings
# Clone the repository
git clone https://github.com/SentinelOps-CI/security-envelopes/security.git
# Install Lean
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
# Install Rust
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
# Install Python dependencies
pip install -r requirements.txt
# Build the project
lake build
cargo build --release# Run all test suites
lake test
cargo test
pytest tests/
# Run specific formal verification
lake test Spec.Tests.RBAC
lake test Spec.Tests.Tenant
lake test Spec.Tests.Attest
# Run chaos testing
docker-compose -f docker-compose.jepsen.yml up -d
./chaos-scripts/network-partition.sh# Generate policy from YAML
cargo run --bin rbac-gen -- examples/01_basic/policy.yaml
# Verify attestation quote
cargo run --bin attest-verify -- quote.bin
# Generate compliance bundle
python bundle/gen.py --output compliance.zip
# Use language bindings
go run examples/go/main.go
node examples/node/main.js
python examples/python/main.pysecurity-envelopes/
├── Spec/ # Lean formal specifications
│ ├── RBAC/ # Role-based access control
│ │ ├── Core.lean # Principal, Scope, Permission definitions
│ │ ├── Policy.lean # Policy evaluation and enforcement
│ │ ├── ABAC.lean # Attribute-based access control
│ │ └── Proofs.lean # Formal correctness proofs
│ ├── Tenant/ # Multi-tenant isolation
│ │ ├── Isolation.lean # Namespace isolation model
│ │ ├── Quotas.lean # Resource quota management
│ │ └── Proofs.lean # Isolation invariant proofs
│ ├── Attest/ # Remote attestation
│ │ ├── SGX.lean # Intel SGX quote verification
│ │ ├── SEV.lean # AMD SEV-SNP attestation
│ │ └── Proofs.lean # Cryptographic correctness
│ └── Tests/ # Formal test suites
│ ├── RBAC.lean # RBAC property tests
│ ├── Tenant.lean # Isolation property tests
│ └── Attest.lean # Attestation property tests
├── engine/ # PolicyEngine WASM runtime
│ ├── src/ # Rust implementation
│ │ ├── policy.rs # Policy definition and evaluation
│ │ ├── wasm.rs # WASM runtime integration
│ │ ├── attest.rs # Attestation verification
│ │ ├── crypto.rs # Cryptographic operations
│ │ └── error.rs # Error handling
│ ├── include/ # C headers for bindings
│ │ └── policyengine.h # C API interface
│ └── examples/ # Runtime examples
├── bundle/ # Compliance bundle generator
│ ├── gen.py # Main bundle generator
├── bindings/ # Language bindings
│ ├── go/ # Go language bindings
│ │ ├── policyengine.go # Go interface
│ │ └── go.mod # Go module definition
│ ├── node/ # Node.js bindings
│ │ ├── src/lib.rs # Rust implementation
│ │ ├── package.json # NPM package
│ │ └── Cargo.toml # Rust dependencies
│ └── python/ # Python bindings
│ ├── policyengine.py # Python interface
│ ├── setup.py # Package setup
│ └── Cargo.toml # Rust dependencies
├── examples/ # Example implementations
├── tests/ # Integration test suites
├── chaos-scripts/ # Chaos testing framework
│ └── network-partition.sh # Network partition simulation
├── ci/ # CI/CD configuration
│ └── workflows/ # GitHub Actions workflows
├── docker/ # Docker configurations
├── lakefile.lean # Lean build configuration
├── Cargo.toml # Rust workspace configuration
├── requirements.txt # Python dependencies
└── README.md # This file
- Formal Verification: All security properties must have machine-checked proofs in Lean
- Memory Safety: Zero unsafe code in Rust components
- Test Coverage: Minimum 95% coverage across all components
- Static Analysis: All code must pass clippy, mypy, and security scanners
- Performance: Sub-millisecond policy evaluation latency
- Documentation: Comprehensive API documentation with examples
- Fork the repository
- Create a feature branch (
git checkout -b feature/amazing-feature) - Implement with formal proofs for security properties
- Add comprehensive tests including chaos testing
- Update documentation and examples
- Ensure all CI checks pass
- Submit a pull request with detailed description
The project uses a comprehensive CI/CD pipeline with the following stages:
- Build: Multi-platform builds (Ubuntu, macOS, Windows)
- Test: Unit tests, integration tests, and formal verification
- Fuzz: Property-based testing with AFL++
- Benchmark: Performance regression testing
- Security: SAST, dependency scanning, and SBOM generation
- Compliance: Automated compliance bundle generation
- Release: Automated releases with signed artifacts
All security properties are formally verified in Lean 4:
- RBAC Soundness: Policies cannot be bypassed
- RBAC Completeness: All valid access is permitted
- Non-Interference: Tenant isolation is preserved
- Decidability: Policy evaluation always terminates
- Monotonicity: Adding permissions cannot reduce access
- ABAC Correctness: Attribute evaluation is sound
- Chaos Testing: Jepsen framework for distributed system testing
- Fuzz Testing: AFL++ for property-based testing
- Static Analysis: Multiple SAST tools integration
- Dependency Scanning: Automated vulnerability detection
- SBOM Generation: Software bill of materials for compliance
- Policy Evaluation: < 25μs overhead at 10,000 requests/second
- WASM Module Size: 200kB total footprint
- Memory Usage: < 1MB per policy engine instance
- Startup Time: < 100ms cold start
- Formal Proof Compilation: < 3 seconds for all proofs
- Multi-Tenant: Support for 1,000+ tenants with isolation guarantees
- Horizontal Scaling: Stateless policy engines for load balancing
- Caching: Intelligent policy caching for repeated evaluations
- Batch Processing: Efficient batch policy evaluation
- OWASP: Complete access control test suite compliance
- NIST: Cryptographic algorithm validation
- SOC 2: Automated evidence collection
- GDPR: Data protection and privacy controls
- HIPAA: Healthcare data security requirements
- Policy Changes: Immutable audit log of all policy modifications
- Access Decisions: Complete record of access control decisions
- Attestation Events: Cryptographic proof of system integrity
- Compliance Bundles: Self-contained audit packages
This project is licensed under the MIT License - see the LICENSE file for details.
- Lean Prover - Formal verification framework
- OWASP - Security testing guidelines
- Jepsen - Distributed systems testing
- Intel SGX - Software Guard Extensions
- AMD SEV - Secure Encrypted Virtualization
- Wasmtime - WebAssembly runtime
- Rust - Memory-safe systems programming
| Component | Status | Performance |
|---|---|---|
| RBAC Core | Complete | security-envelopes < 25μs |
| Multi-Tenant Isolation | Complete | security-envelopes Zero leaks |
| Remote Attestation | Complete | security-envelopes < 10ms |
| PolicyEngine WASM | Complete | security-envelopes 200kB |
| Compliance Bundle | Complete | security-envelopes Automated |
| Language Bindings | Complete | security-envelopes Native performance |
| Chaos Testing | Complete | security-envelopes Jepsen validated |
Security Notice: This software has undergone formal verification and extensive security testing. However, it is recommended to conduct additional security reviews before production deployment in critical environments.