Announcement: VEKOS, an OS with Built-In Cryptographic Proofs
Posted: Wed Dec 04, 2024 10:29 am
VEKOS(Verified Experimental Kernel OS) is a Rust-based experimental kernel that focuses on runtime verification and security. Every filesystem operation and memory allocation generates cryptographic proofs that can be verified in real-time, ensuring system integrity. Think of it like a blockchain for OS operations rather than just storage verification.
Key features:
- Merkle tree-backed filesystem with operation verification
- Memory manager with CoW and proof generation
- Buddy allocator with zone-based memory management
- Shell with VT100 support
- Verified boot sequence with stage attestation
The kernel is still in alpha, but it demonstrates a novel approach to OS security by making verification a first-class citizen. All critical operations (memory allocations, filesystem writes, process creation) generate proofs that are stored in an append-only chain, similar to a blockchain but for system operations.
GitHub: https://github.com/JGiraldo29/vekos
I would be excited to get feedback on this project, especially on the verification approach and potential use cases. If you have any question the innerworkings of the development, just ask and I will gladly answer all questions. The code is under the Apache 2.0 license and welcomes contributors.
Key features:
- Merkle tree-backed filesystem with operation verification
- Memory manager with CoW and proof generation
- Buddy allocator with zone-based memory management
- Shell with VT100 support
- Verified boot sequence with stage attestation
The kernel is still in alpha, but it demonstrates a novel approach to OS security by making verification a first-class citizen. All critical operations (memory allocations, filesystem writes, process creation) generate proofs that are stored in an append-only chain, similar to a blockchain but for system operations.
GitHub: https://github.com/JGiraldo29/vekos
I would be excited to get feedback on this project, especially on the verification approach and potential use cases. If you have any question the innerworkings of the development, just ask and I will gladly answer all questions. The code is under the Apache 2.0 license and welcomes contributors.