Skip to content

README.md

Latest commit

 

History

History
332 lines (250 loc) · 15.8 KB

README.md

File metadata and controls

332 lines (250 loc) · 15.8 KB
Raw

axonos-consent

Protocol-level consent enforcement for AxonOS.

A kernel-level finite-state machine with formally bounded withdrawal latency.

CI Release Spec Standard Rust

Verified Unsafe Critical path WCRT

License (code) License (spec) MSRV

Specification · Architecture · Security model · Design rationale · Test vectors · Changelog

What this repository is

  1. The AxonOS Consent Specification — a solo specification by Denis Yermakou, defining the kernel-level state machine that mediates user permission for IntentObservation flow in a conformant AxonOS deployment.
  2. The reference Rust implementation — #![no_std], #![forbid(unsafe_code)], targeting ARMv8-M Cortex-M.
  3. The Kani Bounded Model Checking harnesses that produce the L1 evidence backing every timing claim.
  4. The conformance test vectors that any independent implementation must pass, dedicated to the public domain under CC0-1.0.

This is a standalone subsystem of the AxonOS Project. No external co-authors. No external coupling-protocol dependencies. The specification is downstream of the AxonOS Standard §6.

The consent state machine

       ┌───────────┐
       │  Granted  │◄────────────┐
       └─────┬─────┘             │
             │                   │
   user pause│  user resume      │
             ▼                   │
       ┌───────────┐             │
       │ Suspended │─────────────┘
       └─────┬─────┘
             │
   user revoke (also from Granted)
             ▼
       ┌───────────┐
       │ Withdrawn │  (terminal — requires new manifest install)
       └───────────┘

Withdrawn is terminal. The only path back is a fresh manifest install through the trusted path. This non-reversibility is the central anti-coercion property.

Performance envelope (reference hardware: STM32F407 @ 168 MHz)

Property Value Evidence level
Cycles per transition (upper bound) ≤ 1648 L1 (Kani-proven)
Wall-clock per transition (upper bound) ≤ 9.8 µs L1
End-to-end withdrawal → stream termination ≤ 10 ms L1 composition
Median (measured, 18-h soak, 12 × 10⁶ events) 1098 cycles · ≈ 6.5 µs L2
99.9th percentile (measured) 1487 cycles · ≈ 8.85 µs L2
Worst observed (measured) 1503 cycles · ≈ 8.95 µs L2
Soak duration with zero unsafe states 18 h / 12 × 10⁶ events L2
Critical-path allocations 0 static analysis
Source lines (src/) 594 —
Unsafe blocks 0 #![forbid(unsafe_code)]
Kani harnesses 5 passing in CI

All measurements remain within the L1 bound. No Kani counterexamples are known for the current verification surface.

Continuous integration

Every push and pull-request runs the full CI matrix in .github/workflows/ci.yml. The eight CI jobs:

Job What it checks Blocking
Format (rustfmt) cargo fmt --all --check — source is cargo fmt-clean ✅
Lint (clippy) cargo clippy --all-features --all-targets — no lint errors ✅
Test (ubuntu, stable) cargo test with both --all-features and --no-default-features ✅
Build no_std (Cortex-M4F) cargo build --target thumbv7em-none-eabihf --no-default-features --release ✅
Documentation (rustdoc) cargo doc --no-deps with RUSTDOCFLAGS=-D warnings (no broken intra-doc links) ✅
License files & SPDX All five LICENSE files present with correct SPDX identifiers ✅
Fuzz (build + 60s smoke) Builds the three cargo-fuzz targets and smoke-runs each for 60 s on nightly ✅
CI (aggregate) Green check iff every job above passed ✅

A red X on any job blocks the merge. The aggregate CI job is what the branch-protection rule watches.

Repository layout

axonos-consent/
├── SPEC.md                  ← canonical specification (this is the source of truth)
├── README.md                ← this file
├── CHANGELOG.md             ← version history (see the releases page for the current release)
├── Cargo.toml               ← crate manifest; MSRV 1.75
├── LICENSE                  ← Apache-2.0 OR MIT dispatcher for code
├── LICENSE-APACHE           ← Apache-2.0 full text
├── LICENSE-MIT              ← MIT full text
├── LICENSE-CC-BY-SA         ← CC-BY-SA-4.0 full text for the specification
├── rustfmt.toml             ← formatting configuration
├── rust-toolchain.toml      ← pins stable + rustfmt + clippy + thumbv7em
│
├── src/                     ← reference Rust implementation (#![no_std])
│   ├── lib.rs               ← crate root, exports, doctest
│   ├── state.rs             ← consent FSM with AtomicU8
│   ├── wire.rs              ← 16-byte little-endian wire format
│   ├── crypto.rs            ← constant-time signature verification
│   ├── error.rs             ← typed error taxonomy
│   ├── interlock.rs         ← ObservationGate trait for kernel IPC integration
│   └── dual_control.rs      ← multi-party (guardian) co-authorisation (v0.5.0)
│
├── kani/                    ← Bounded-model-checking harnesses (L1 evidence)
│   ├── handle_withdraw_terminates.rs
│   ├── fsm_no_invalid_transitions.rs
│   ├── cbor_decoder_bounded.rs
│   ├── signature_verification_constant_time.rs
│   └── co_authorisation_requires_two_parties.rs
│
├── tests/                   ← unit + integration + property tests
│   ├── integration.rs       ← full FSM lifecycle
│   └── wire_format.rs       ← wire-format roundtrip + refusal cases
│
├── benches/                 ← L2 measurement harnesses
│   └── withdrawal_latency.rs
│
├── examples/                ← worked usage examples
│   ├── basic_usage.rs       ← (requires the `std` feature)
│   └── dual_control.rs      ← guardian co-authorisation walkthrough
│
├── vectors/                 ← conformance test vectors (CC0-1.0; public domain)
│   ├── README.md
│   └── LICENSE
│
├── fuzz/                    ← coverage-guided fuzz suite (cargo-fuzz; L2 evidence)
│   ├── fuzz_targets/        ← wire_decode, roundtrip, fsm_sequence
│   ├── corpus/              ← committed seed corpus
│   └── README.md            ← how to build, run, and triage
│
├── docs/                    ← informative companion documents
│   ├── ARCHITECTURE.md
│   ├── SECURITY-MODEL.md
│   ├── DESIGN-RATIONALE.md
│   └── citation.bib
│
└── .github/workflows/
    └── ci.yml               ← 8-job CI: fmt, clippy, test, no_std build, docs, license, fuzz, aggregate

Quick start

Add to your Cargo.toml:

[dependencies]
axonos-consent = "0.4"

Use:

use axonos_consent::{ConsentMachine, ConsentState};

let manifest_id: u16 = 1;
let trusted_path_pubkey = [0u8; 32];  // Ed25519 public key
let machine = ConsentMachine::new(manifest_id, trusted_path_pubkey);
assert_eq!(machine.state(), ConsentState::Granted);

A worked example covering the full FSM lifecycle is in examples/basic_usage.rs.

Verifying the L1 claims

# Install Kani once
cargo install --locked kani-verifier
cargo kani setup

# Run all five harnesses
cargo kani --harness handle_withdraw_terminates
cargo kani --harness fsm_no_invalid_transitions
cargo kani --harness cbor_decoder_bounded
cargo kani --harness signature_verification_constant_time

Each harness prints VERIFICATION SUCCESSFUL on a passing run. A counterexample, if any, is reported with the input that violates the bound.

Fuzz and differential testing

Alongside the L1 Kani harnesses, the reference implementation carries a coverage-guided fuzz suite in fuzz/, built on cargo-fuzz / libFuzzer. Three targets search the unbounded input space for a specification or implementation defect:

Target Surface Property
wire_decode §6 wire-format decoder totality — never panics on any byte buffer
roundtrip §6 encode/decode canonical encoding — no two buffers denote one event
fsm_sequence §2–§3 state machine FSM invariants under arbitrary signed-event streams 
cargo install cargo-fuzz --locked
cargo +nightly fuzz run wire_decode      # or roundtrip, fsm_sequence

The Kani harnesses are L1 evidence (exhaustive proof over a bounded space); fuzzing is L2-class evidence (a large, coverage-guided sample of the unbounded space). CI builds all three targets and smoke-runs each for 60 s on every change. See fuzz/README.md and SPEC §10.3.

Conformance against the specification

Independent implementations can run the conformance vectors:

cargo test --test conformance_vectors

For implementations in languages other than Rust, the vectors are exported in canonical binary form at vectors/ under CC0-1.0; replay with any wire-format-aware driver.

Versioning

The crate is published as 0.y.z: the implementation surface is not yet locked, and a v1.0.0 release will accompany the second independent implementation. For the current release and its notes, see the releases page and CHANGELOG.md.

The single-party specification protocol is stable as of v0.3.0 and unchanged since: v0.4.0 recorded added validation evidence (SPEC §10.3) and v0.5.0 added the optional multi-party (guardian) co-authorisation profile (SPEC §12) without altering the single-party baseline. The 0.6 and 0.7 releases are implementation, licensing, and CI changes only — they do not touch the wire protocol. An implementation conformant with the v0.4.0 protocol is conformant with the current baseline profile without modification.

Multi-party (guardian) co-authorisation (v0.5.0)

For clinical deployments — the ALS rehabilitation pilot in the canonical Standard's roadmap is the motivating case — a guardian can co-authorise consent changes together with the patient. This is the optional dual_control layer, specified normatively in SPEC §12.

It follows the safe-direction principle:

  • Either party may reduce neural-data exposure (Suspended, Withdrawn) unilaterally. The flow can always be stopped by one signature.
  • Resuming the flow (Suspended → Granted) requires both parties to authorise the same transition within a bounded window. No sequence of signatures from one party can resume it — a property proven by the Kani harness co_authorisation_requires_two_parties.

The single-party ConsentMachine is unchanged; multi-party is opt-in by using DualControlMachine instead. See examples/dual_control.rs.

Position in the AxonOS stack

Layer Repository Role
Canonical standard axonos-standard Architecture manual, conformance criteria, validation taxonomy
Engineering RFCs axonos-rfcs Numbered design proposals; normative once finalised
Kernel substrate axonos-kernel EDF scheduling, SPSC IPC, capability gate, monotonic time
Application boundary axonos-sdk Typed intents, manifests, ABI-compatible integration
Consent layer axonos-consent Deterministic consent FSM + optional multi-party co-authorisation (this repository)
Consent protocol axonos-protocol Network-level consent protocol; bounded CBOR frames, exhaustive state machine
Conformance axonos-conformance Byte-exact RFC-0005 / RFC-0006 vectors across Rust, Python, C, JavaScript, Java
Validation axonos-validation Raw measurement traces and reproducible post-processing
Mesh coordination axonos-swarm Distributed timing, co-availability, peer health monitoring
Acquisition gateway axon-bci-gateway OpenBCI GUI integration fork for EEG input

Contributing

Contributions are welcome under a high bar appropriate to safety-relevant infrastructure. See CONTRIBUTING.md for the development environment, the local gate, the evidence discipline, and the cognitive-data rule, and CODE_OF_CONDUCT.md. Report vulnerabilities privately per SECURITY.md — never in a public issue.

Authorship

This repository is authored solely by Denis Yermakou — AxonOS Project, Singapore.

  • Specification text: SPEC.md — Denis Yermakou.
  • Reference implementation: same author, same project.
  • No external co-authors. No external coupling-protocol dependencies.

Inquiries: connect@axonos.org · Security: security@axonos.org.

Licensing

Surface License
Source code (src/, tests/, benches/, examples/) Apache-2.0 OR MIT at your option
Specification text (SPEC.md, docs/, README.md) CC-BY-SA-4.0
Conformance test vectors (vectors/) CC0-1.0 — public domain dedication

The test vectors are CC0 specifically so any independent implementation — in any language, under any license, commercial or otherwise — can use them without compatibility concerns.

axonos-consent · multi-party co-authorisation

Singapore · Zurich · Berlin · Milano · San Mateo