I finished the first full pass of mechanically verified Rust proofs, all 11 checks done and verifier-backed. The post walks through what that actually means: the Coq work, Kani, fuzzing, the test suite, where the proof boundaries sit, and what's still on the table. Merkle soundness, non-empty revocation witnesses, encode/decode round-trips, and the seal/open semantics are all coming next.

#RustLang #FormalVerification #Kani #Cryptography

https://oreulius.com/blog/project-update-formal-verification-fuzzing-and-tests-of-the-arc-encryption-schem

Oreulius’s compositor ends raw framebuffer access by wrapping drawing in capabilities. The new path adds policy and audit; the legacy one preserves demos. CVE‑2024‑46826 shows how ELF loader bugs like double reading randomize_va_space cause unpredictable behaviour. Memory‑safe Rust and strict capability checks are essential.

#CapabilityBasedSecurity #MicrokernelArchitecture #TrustedDisplayServer #OreuliusOS
https://oreulius.com/blog/code-review-the-compositor

Kernel cryptography review: the crypto folder was the least mature part of this pass, so the review focused on plumbing it correctly into capability authority, typed trust data, key derivation, Ed25519 verification, and AES-GCM sealing.

https://oreulius.com/blog/code-review-the-crypto-folder

#OSDev #Cryptography #KernelEngineering #SystemSecurity

Execution engine review: this one is long because ELF loading, WASM runtime behavior, binary loading, JIT paths, traps, and portability can introduce a lot of subtle kernel bugs.

This post looks at what still needs to be implemented before the execution engine should be pushed through the final dev cycle, after the architecture and abstraction layer.

How do you handle portability testing near the end of an OS dev cycle?

#Wasm #KernelDev #SystemsProgramming
https://oreulius.com/blog/code-review-the-wasm-runtime-and-elf-execution-engine

Introducing ReKurn; A git like version control system, + securable decentralized log in system and authentication system for node.js npm and typescript heavy sites.

Built originally for the Oreulius site to host our own code, repos, packages, and oreulius applications be they open source, source available, as a binary that rekurn will one day be able to install.

Allows authentication where necessary against a site + Many plans for the oreulius ecosystem with this.

https://github.com/reeveskeefe/Rekurn

Heres the explanation of why I went with the name Oreulius, it is not simply a name based off similarities, it is a name I chose as a unified design principle

#kernel #OS #namechoice #development

https://oreulius.com/blog/why-i-went-with-the-name-oreulius

This is the first code review of the capability system in the oreulius kernel, as-well as what isn't complete, what is complete, and assuring it has the design premise that is intended. As-well, I have done a thorough analysis of the attack surface potential and how they were mitigated, and if they have been mitigated.

#rust #capabilitysystem #OSDEV #Kernel #development

Read the blog on this here:
https://oreulius.com/blog/code-review-the-oreulius-capability-capnet-and-its-provenance-graph

The second code review has been completed.

It's important that the architectural and abstraction layer remains as small as possible and bridged between assembly and rust so that the rust code stays as isolated from the machine as possible. so its more than just memory safe, it is memory secured!

But there are some big changes that can be made without changing or drastically increasing the size of the abstraction and architectural layer.

The related blog is here:

https://www.oreulius.com/blog/code-review-the-architecture-and-abstraction-layer-arch