jsecmon: first verified kernel — dga::max_consonant_run in Typed Jerboa
Jaime Fournier <jaimef@linbsd.org>
3df4d37c12511e033c8a539f6570f9279d598e14
new file mode 100644 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +# Generated Rust crate (regenerate with `make rust`). +/build/ new file mode 100644 --- /dev/null +++ b/Makefile @@ -0,0 +1,26 @@ +# jsecmon — pure-Jerboa reimplementation of secmon. +# +# Security-critical kernels live in typed/*.ss as Typed Jerboa and are compiled +# to a Rust crate by the jerboa typed→rust backend, then verified against +# secmon's own test vectors (tests/*.rs). +JERBOA ?= $(HOME)/mine/jerboa +SCHEME ?= $(JERBOA)/.chez/bin/scheme +BUILD ?= build/rust +TYPED := $(wildcard typed/*.ss) + +.PHONY: rust test clean + +# Generate the Rust crate from the Typed Jerboa kernels, then drop in the +# hand-written verification tests (the generator only writes src/ + Cargo.toml). +rust: + cd $(JERBOA) && $(SCHEME) --libdirs lib --script support/typed-rust.ss \ + $(CURDIR)/$(BUILD) $(addprefix $(CURDIR)/,$(TYPED)) + @mkdir -p $(BUILD)/tests + @cp tests/*.rs $(BUILD)/tests/ + +# Verify the generated kernels against secmon's vectors. +test: rust + cd $(BUILD) && cargo test + +clean: + rm -rf $(BUILD) new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,41 @@ +# jsecmon + +A pure-[Jerboa](../jerboa) reimplementation of [`secmon`](../secmon), a host +security monitor. The goal: no hand-written Rust or C. Security-critical kernels +(crypto, secrets, detection scoring) are written in **Typed Jerboa** and +compiled to Rust by jerboa's typed→rust backend; the rest is ordinary Jerboa. + +This is a long, incremental port. Each kernel is translated, compiled to Rust, +and **verified against secmon's own test vectors** before it counts as done. + +## Layout + +``` +typed/ Typed Jerboa kernels (.ss) — compile to a Rust crate +tests/ Hand-written Rust tests asserting parity with secmon's vectors +build/rust/ Generated crate (gitignored; `make rust` regenerates) +``` + +## Build & verify + +``` +make rust # typed/*.ss → build/rust (a cargo crate) +make test # regenerate, then cargo test against secmon's vectors +``` + +`make` needs a built jerboa checkout at `$JERBOA` (default `~/mine/jerboa`), +whose `.chez/bin/scheme` and `support/typed-rust.ss` drive the backend. + +## Port status + +Driven by what each module needs from the backend; pure-logic detection first, +then crypto orchestration, then I/O / async / FFI (monitors, server, storage). + +| secmon module | jsecmon | status | +|--------------------------|--------------------|---------------------------------| +| `dga::max_consonant_run` | `typed/dga.ss` | ✅ ported, vectors pass | +| `dga::shannon_entropy` | `typed/dga.ss` | ⏳ needs backend f64 `log2` | +| `dga::score_domain` | `typed/dga.ss` | ⏳ after entropy + string ops | +| `lolbin`, `sigma`, `triage` | — | ⏳ pure logic, queued | +| `crypto::{psk,ecies}` | — | ⏳ FFI-delegated; orchestration only | +| monitors / server / storage / ebpf / dtrace | — | ⏳ I/O+async+FFI, last | new file mode 100644 --- /dev/null +++ b/tests/dga_vectors.rs @@ -0,0 +1,17 @@ +// Verifies the Typed-Jerboa-generated dga kernel against secmon's own +// dga::tests vectors (secmon/src/dga.rs). `make rust` copies this file into +// the generated crate's tests/ dir before `cargo test`. +use jerboa_typed_generated::jsecmon_dga::max_consonant_run; + +#[test] +fn consonant_run_matches_secmon_vectors() { + assert_eq!(max_consonant_run("hello".to_string()), 2); + // "strengths" — after the 'e', n-g-t-h-s = 5 consonants + assert_eq!(max_consonant_run("strengths".to_string()), 5); + assert_eq!(max_consonant_run("xkqzmnpw".to_string()), 8); + assert_eq!(max_consonant_run("aeiou".to_string()), 0); + // empty label → 0 + assert_eq!(max_consonant_run("".to_string()), 0); + // uppercase folds the same as lowercase + assert_eq!(max_consonant_run("STRENGTHS".to_string()), 5); +} new file mode 100644 --- /dev/null +++ b/typed/dga.ss @@ -0,0 +1,41 @@ +;;; jsecmon — DGA (Domain Generation Algorithm) detection kernels. +;;; +;;; Pure scoring logic ported from secmon/src/dga.rs to Typed Jerboa, compiled +;;; to Rust by the jerboa typed→rust backend. Domains are ASCII, so we score +;;; over UTF-8 bytes (string->utf8 + bytevector-u8-ref) rather than chars. +(typed-library (jsecmon dga) + (export max-consonant-run) + + ;; Running state for the consonant-run fold: the current run length and the + ;; longest run seen so far. A record accumulator lets a single-accumulator + ;; for/fold carry both values (no multi-accumulator support needed). + (record CrState + ((run : Nat) + (best : Nat))) + + ;; ASCII lowercase: map A-Z (65..90) into a-z by setting bit 0x20. + (def (ascii-lower (b : Nat)) : Nat + (if (and (>= b 65) (<= b 90)) + (+ b 32) + b)) + + ;; A consonant is an ASCII letter that is not one of aeiouy (matching + ;; secmon's Unicode-naive rule). Vowel codes: a=97 e=101 i=105 o=111 u=117 y=121. + (def (ascii-consonant? (b : Nat)) : Bool + (let ((lc (ascii-lower b))) + (and (>= lc 97) + (<= lc 122) + (not (or (= lc 97) (= lc 101) (= lc 105) + (= lc 111) (= lc 117) (= lc 121)))))) + + ;; Longest run of consecutive ASCII consonants in s; vowels and any + ;; non-letter reset the run. Mirrors dga::max_consonant_run. + (def (max-consonant-run (s : String)) : Nat + (let ((bs (string->utf8 s))) + (CrState-best + (for/fold ((st (make-CrState 0 0))) + ((i (in-range (bytevector-length bs)))) + (if (ascii-consonant? (bytevector-u8-ref bs i)) + (let ((r (+ (CrState-run st) 1))) + (make-CrState r (if (> r (CrState-best st)) r (CrState-best st)))) + (make-CrState 0 (CrState-best st))))))))