Skip to content

Commit 70a5a8c

Browse files
committed
chore: updated readme and added figurative assets
1 parent dd85a92 commit 70a5a8c

4 files changed

Lines changed: 69 additions & 75 deletions

File tree

README.md

Lines changed: 69 additions & 75 deletions
Original file line numberDiff line numberDiff line change
@@ -1,51 +1,75 @@
1-
This repository reflects the v0.3.0-alpha research prototype described in the submitted manuscript
2-
*"Proportional-Cost Per-Read Provenance: Making Continuous File Integrity Verification Affordable on Edge Hardware."*
1+
<p align="center">
2+
<img src="assets/axiom-banner.png" alt="Axiom OS" width="100%">
3+
</p>
34

4-
# Axiom OS
5+
<p align="center">
6+
<img src="https://img.shields.io/badge/license-MIT%20%2F%20Apache--2.0-blue" alt="License">
7+
<img src="https://img.shields.io/badge/rust-no__std-orange" alt="Rust no_std">
8+
<img src="https://img.shields.io/badge/arch-x86__64%20%7C%20aarch64-lightgrey" alt="Architecture">
9+
<img src="https://img.shields.io/badge/status-research%20prototype-yellow" alt="Status">
10+
</p>
511

6-
A bare-metal `no_std` Rust kernel that enforces BLAKE3 file-integrity provenance on **every read**
7-
not just at load time — and makes that affordable by verifying only the file blocks a read actually touches.
12+
<!-- Add a CI badge ONLY if the workflow is green:
13+
![CI](https://github.com/abhiprd2000/axiom-os-kernel/actions/workflows/code.yml/badge.svg)
14+
-->
815

9-
## Core Contribution
16+
> This repository is the `v0.3.0-alpha` research prototype described in the manuscript
17+
> *"Proportional-Cost Per-Read Provenance: Making Continuous File Integrity Verification Affordable on Edge Hardware,"* submitted to IEEE Embedded Systems Letters.
1018
11-
Most integrity mechanisms verify once: at boot, at open, or when a page is first read from storage
12-
(e.g. fs-verity, dm-verity, IMA). After that, the cached in-memory copy is trusted. Axiom re-verifies
13-
the in-memory data on **every** read, so tampering that happens *after* the initial check (a memory bug,
14-
DMA, a row-hammer flip) is caught on the next read.
19+
A bare-metal `no_std` Rust kernel that enforces BLAKE3 file-integrity provenance on **every read** — not just at load time — and makes that affordable by verifying only the file blocks a read actually touches.
1520

16-
The naive way to do this — re-hash the whole file on every read — costs O(file size) per read and is
17-
impractical on small devices. Axiom instead uses **block-level provenance**:
21+
> *No data is better than faulty data.*
1822
19-
- A file is split into fixed 4 KiB blocks; each block has its own stored BLAKE3 leaf hash.
20-
- A ranged read `read_range(offset, len)` maps to the blocks it overlaps and re-hashes **only those blocks**,
21-
comparing each against its stored leaf in constant time. Per-read cost becomes O(bytes read), not O(file size).
22-
- A **lazy Merkle root** over the block leaves gives a single 32-byte commitment to the file; a single-block
23-
write updates one leaf and defers the root recomputation, so writes cost one block hash instead of a full rehash.
23+
---
2424

25-
This is the affordability result: per-read verification cost stays flat regardless of file size (see Results).
25+
## Why
2626

27-
## How it differs from fs-verity / IMA
27+
Most integrity mechanisms verify **once**: at boot, at open, or when a page is first read from storage (fs-verity, dm-verity, IMA). After that, the cached in-memory copy is trusted. If something tampers with that cached page *after* the check — a memory bug, a DMA-capable peripheral, a row-hammer flip — every later read returns the corrupted bytes as authentic. This is a live class of attack (e.g. Dirty Pipe, Copy Fail).
2828

29-
fs-verity and IMA bind verification to the storage-access path — a page is checked when read from the device,
30-
then trusted in the page cache. They do not re-verify the cached copy on subsequent reads. Axiom's check *is*
31-
the read path, on every read, against per-block hashes. See Table II of the paper for the full comparison.
29+
Axiom re-verifies the in-memory data on **every read**, so that tampering is caught on the next read. The naive way to do this — re-hash the whole file each read — costs *O(file size)* per read and is impractical on small devices. Axiom makes it affordable.
30+
31+
## How
32+
33+
<p align="center">
34+
<img src="assets/fig1.png" alt="Per-read block-level verification" width="80%">
35+
</p>
36+
37+
- A file is split into fixed **4 KiB blocks**; each block stores its own BLAKE3 leaf hash.
38+
- A ranged read `read_range(offset, len)` maps to the blocks it overlaps and re-hashes **only those blocks**, comparing each against its stored leaf in constant time. Per-read cost becomes *O(bytes read)*, not *O(file size)*.
39+
- A **lazy Merkle root** over the block leaves is a single 32-byte commitment to the file; a single-block write updates one leaf and defers the root recomputation, so a write costs one block hash instead of a full rehash.
40+
41+
Unlike out-of-band detectors that periodically re-scan files, Axiom enforces integrity **inline** on the read path — every read is verified before its bytes are returned, leaving no detection window.
42+
43+
## Results
44+
45+
Per-read **block-level verification is constant** regardless of file size — about **2.7 µs** (x86-64) and **3.65 µs** (ARM64) — while whole-file verification grows with size. Median wall-clock times on real hardware, from the `bench-native` harness:
46+
47+
| File size | Blocks | x86-64 whole (ms) | x86-64 block (ms) | ARM64 whole (ms) | ARM64 block (ms) |
48+
|-----------|-------:|------------------:|------------------:|-----------------:|-----------------:|
49+
| 4 KiB | 1 | 0.0035 | 0.0027 | 0.0036 | 0.0037 |
50+
| 16 KiB | 4 | 0.0094 | 0.0033 | 0.0143 | 0.0037 |
51+
| 64 KiB | 16 | 0.0339 | 0.0030 | 0.0570 | 0.0037 |
52+
| 256 KiB | 64 | 0.108 | 0.0027 | 0.228 | 0.0037 |
53+
| 1 MiB | 256 | 0.555 | 0.0027 | 0.918 | 0.0037 |
54+
| 4 MiB | 1024 | 2.13 | 0.0026 | 3.72 | 0.0037 |
55+
56+
At 4 MiB, block-level verification is **~810× cheaper** (x86-64) and **~1020× cheaper** (ARM64) than whole-file.
57+
58+
**Hardware:** x86-64 = Intel Core i5-5200U (Linux, `rustc` 1.96-nightly); ARM64 = Qualcomm Snapdragon 7 Gen 4 (Cortex-A720/A520), Termux on Android 16 (`rustc` 1.95). Both use `blake3` v1.8.5 with runtime SIMD.
3259

3360
## Architecture
3461

3562
- **Target:** x86_64 (primary) + ARM64 (QEMU `virt`)
3663
- **Language:** Rust (`no_std`, no libc)
37-
- **Source:** ~3,600 lines across 36 files
38-
- **Release:** v0.3.0-alpha (research prototype)
39-
40-
**Kernel subsystems:** GDT/IDT, 8 MB linked-list heap, priority scheduler, per-process page tables
41-
(CR3 isolation), IPC message queues, ATA PIO driver, syscall interface (INT 0x80), interactive shell.
64+
- **Release:** `v0.3.0-alpha` (research prototype)
4265

4366
**Provenance layer:**
44-
- `vfs.rs` — per-block BLAKE3 leaves, `read_range`/`verify_range` (verify only touched blocks),
45-
`write_block` + lazy `merkle_root`, `constant_time_eq` comparison.
46-
- `provenance.rs``provenance_hash` (BLAKE3) and constant-time comparison primitive.
67+
- `vfs.rs` — per-block BLAKE3 leaves; `read_range` / `verify_range` (verify only touched blocks); `write_block` + lazy `merkle_root`.
68+
- `provenance.rs``provenance_hash` (BLAKE3) and a constant-time comparison primitive.
4769
- `fat32.rs` — on-disk hash store for the persistent path.
48-
- `mitra/` — small DSL whose `trusted_data` type routes through the verified read path.
70+
- `mitra/` — a small DSL whose `trusted_data` type routes through the verified read path.
71+
72+
**Kernel subsystems:** GDT/IDT, 8 MB linked-list heap, priority scheduler, per-process page tables (CR3 isolation), IPC queues, ATA PIO driver, syscall interface (INT 0x80), interactive shell.
4973

5074
## Quick Start
5175

@@ -59,11 +83,11 @@ sudo apt install qemu-system-x86 qemu-system-arm nasm
5983
# Boot x86_64 (use the bin target; plain `cargo build` also tries the ARM bin)
6084
cargo run --bin axiom_os
6185

62-
# Boot ARM64
86+
# Boot ARM64 (QEMU virt)
6387
./run_arm.sh
6488
```
6589

66-
## Tamper-Detection Demo
90+
### Tamper-detection demo
6791

6892
Inside the booted shell:
6993

@@ -74,62 +98,32 @@ tamper secret # flip a byte in memory
7498
cat secret # -> READ BLOCKED: provenance violation
7599
```
76100

77-
## Results
78-
79-
The headline result is **proportional access**: block-level verification cost is constant (~3.6 µs)
80-
across file sizes, while whole-file verification grows with size. Numbers below are **median wall-clock
81-
times on real hardware** (a commodity x86-64 laptop and a mobile-class ARM64 core), produced by the
82-
standalone `bench-native` harness:
83-
84-
| File size | Blocks | x86-64 whole (ms) | x86-64 block (ms) | ARM64 whole (ms) | ARM64 block (ms) |
85-
|---|---|---|---|---|---|
86-
| 4 KiB | 1 | 0.0040 | 0.0037 | 0.0037 | 0.0037 |
87-
| 16 KiB | 4 | 0.0097 | 0.0033 | 0.0143 | 0.0037 |
88-
| 64 KiB | 16 | 0.046 | 0.0035 | 0.057 | 0.0037 |
89-
| 256 KiB | 64 | 0.159 | 0.0037 | 0.230 | 0.0037 |
90-
| 1 MiB | 256 | 0.580 | 0.0035 | 0.923 | 0.0037 |
91-
| 4 MiB | 1024 | 2.51 | 0.0039 | 3.74 | 0.0037 |
92-
93-
Block-level verification is >640× cheaper (x86-64) and >1000× cheaper (ARM64) than whole-file at 4 MiB.
101+
### Reproducing the benchmark numbers
94102

95-
Reproduce the real-hardware numbers:
103+
`bench-native` is a `std` crate that lives inside this `no_std` kernel repo, so it inherits the kernel's bare-metal cargo config. **Build it outside the kernel tree:**
96104

97105
```bash
98-
cd bench-native
99-
cargo run --release # prints the whole-file vs block table for this CPU
106+
cp -r bench-native /tmp/axiom-bench && cd /tmp/axiom-bench
107+
cargo run --release # prints the whole-file vs block table + inline-vs-periodic comparison
100108
```
101109

102-
Reproduce the in-kernel proportional ratio under emulation:
110+
To reproduce the in-kernel proportional *ratio* under emulation, run `bench` in the booted shell (RDTSC size sweep). In-kernel cycle counts are emulated and used only to confirm the ratio; all millisecond figures above are from real hardware.
103111

104-
```
105-
bench # in the booted shell; RDTSC, proportional-access size sweep
106-
```
112+
## Threat Model
107113

108-
**Note on QEMU:** in-kernel cycle counts are emulated and are used only to confirm the *ratio*
109-
(block-flat vs whole-file-growing). All absolute millisecond figures above come from real hardware,
110-
not emulation.
114+
Assumes an adversary who can modify a file's in-memory bytes after they were validated, but cannot forge the stored provenance record (per-block leaves + root). Single-core, no DMA, no ring-0. Within this model, per-read verification **reduces** the TOCTOU window: bytes returned by `read()` are verified at the moment of return. It does **not** eliminate TOCTOU (corruption after a verified read is out of scope), nor address replay/splicing on persistent storage or hardware memory-integrity attacks.
111115

112116
## Limitations
113117

114-
- Boots under QEMU; UEFI bootloader for bare-metal boot is pending.
115-
- Single-core; SMP and multi-core verification are future work.
118+
- Boots under QEMU; a UEFI bootloader for bare-metal boot is pending.
119+
- Single-core; SMP / multi-core verification is future work.
116120
- BLAKE3 runs in portable mode in-kernel (no in-kernel SIMD yet); the native harness uses runtime SIMD.
117-
- Real-hardware results use a consumer laptop and phone; a dedicated embedded SoC (e.g. Raspberry Pi)
118-
measurement is the immediate next step.
119-
120-
## Threat Model
121-
122-
Assumes an adversary who can modify a file's in-memory bytes after they were validated, but cannot forge
123-
the stored provenance record (per-block leaves + root); single-core, no DMA, no ring-0. Within this model,
124-
per-read verification **reduces** the TOCTOU window: bytes returned by `read()` are verified at the moment
125-
of return. It does **not** eliminate TOCTOU (corruption after a verified read is out of scope), nor address
126-
replay/splicing on persistent storage or hardware memory-integrity attacks.
121+
- Real-hardware results use a laptop and a phone; a dedicated embedded SoC (e.g. Raspberry Pi) measurement is the immediate next step.
127122

128123
## Paper
129124

130-
- Earlier formulation (whole-file per-read, equity framing): Zenodo, Apr. 2026,
131-
[doi:10.5281/zenodo.19387932](https://doi.org/10.5281/zenodo.19387932).
125+
- Earlier formulation (whole-file per-read, equity framing): Zenodo, Apr. 2026 — [doi:10.5281/zenodo.19387932](https://doi.org/10.5281/zenodo.19387932)
132126

133127
## License
134128

135-
MIT and Apache-2.0
129+
Dual-licensed under [MIT](LICENSE-MIT) and [Apache-2.0](LICENSE-APACHE).

assets/axiom-banner.png

295 KB
Loading

assets/fig1.png

39.5 KB
Loading

assets/fig2.png

211 KB
Loading

0 commit comments

Comments
 (0)