diff --git a/BUILT.md b/BUILT.md index 807fa9d..5d36df4 100644 --- a/BUILT.md +++ b/BUILT.md @@ -299,10 +299,14 @@ out-of-bounds `inbounds` getelementptr into a constant is poison and LLVM folds wrong answer instead of touching memory. Same family as `(<< 1 32)` compiling to a bare `retq`. **What ASan covers of the bounds checks' job, since `--sanitize --no-bounds-checks` is the run that asks.** Three of -`bounds.flan`'s six deliberate out-of-bounds cases are caught. A negative index into a global is not — a global gets a -right redzone and nothing to its left. Neither is a reversed slice, which computes a negative length and then reads -nothing at all. ASan sees out-of-*object* access, not out-of-subobject, so a slice into the middle of a larger array can -overrun its logical bounds without crossing a redzone at all. It is a second net, not a replacement. +`bounds.flan`'s six deliberate out-of-bounds cases are caught. A negative index into a global is not, and the reason is +layout rather than anything about the access: ASan lays a global out as `{data, redzone}`, so reading before one lands +in whatever precedes it, which is a redzone if something instrumented is there and ordinary memory if nothing is. +Measured both ways — silent in `bounds.flan`, reported as soon as another `defvar` is declared in front of `arr`. A +reversed slice is not caught either, having computed a negative length and read nothing at all. And ASan sees +out-of-*object* access, not out-of-subobject, so a slice into the middle of a larger array can overrun its logical +bounds without crossing a redzone. Three of six is a ceiling on what it covers, not a measurement of the risk. It is a +second net, not a replacement. The sweep lives on its own dune alias rather than on `dune test`: a sanitized program links to a statically linked 1.8MB binary, and twenty-eight of them twice over is minutes against the suite's seconds. diff --git a/NEXT.md b/NEXT.md index bbf519b..196b077 100644 --- a/NEXT.md +++ b/NEXT.md @@ -64,82 +64,35 @@ the commit that made it. ### Landed — the runtime under a sanitizer -`--sanitize` is a build flag beside `--debug`, and `dune build --root . @sanitize` is the sweep: twenty-eight programs -built twice, plain and sanitized, compared on output and exit status. It is not on `dune test` — a sanitized program is -a statically linked 1.8MB binary and the sweep is about nine minutes against the suite's seconds. +`--sanitize` is a build flag beside `--debug`; `dune build --root . @sanitize` builds twenty-eight programs twice, plain +and sanitized, and compares output and exit status. Its own alias and not `dune test`, because the sweep is about nine +minutes. The checked sweep is **clean**. How ASan and UBSan reach a language whose IR is written by hand, and why the +flag does not force `-O0` when `--debug` does, is in [`BUILT.md`](BUILT.md). -**The flag was the easy half. What the sanitizers reach is not symmetric, and this is the thing to remember:** +Two defects came out of it, both found by reading rather than by the tools, both fixed with a regression case: +`flan_bytes_to_i64`/`flan_bytes_to_f64` clamped a slice length with `(size_t)n` and so read 63 or 511 bytes off the end +of a negative-length slice; and the three `snprintf` shims published snprintf's return as a slice length, which is what +it *would* have written. -- **ASan reaches Flan code only because `Emit` now says so.** AddressSanitizer is an LLVM pass but it instruments only - functions carrying the `sanitize_address` attribute, which clang's *C frontend* adds and which nothing adds to IR - written by hand. Before that attribute, `clang -fsanitize=address` over the `.ll` instrumented `flan_rt.c` and not one - instruction of Flan: a read off the end of a `defvar` array in a `--no-bounds-checks` build printed its garbage and - exited 0. With it, the same program reports `global-buffer-overflow in flan.main`. Globals get their redzone from the - module pass either way. `test_sanitize`'s first control is that exact program, so the day the attribute stops being - emitted the sweep fails loudly instead of going quietly green. -- **UBSan reaches the runtime's C and nothing else, and there is no lever for it.** Its checks are branches to - `__ubsan_handle_*` that clang's C frontend emits; no attribute asks a pass to produce them. `(<< 1 32)` under - `-fsanitize=undefined` is still unremarked. **Item 3 of the old plan — shift UB, alignment, the f32→i32 cast on NaN — - is therefore not answerable this way, and is still open.** The choices are to emit the checks from `Emit` behind the - flag (a compiler feature, and the same shape the bounds checks already have) or to leave those to the checker. The - second control in `test_sanitize` is a program with unambiguous shift UB that is expected *not* to be caught, so if a - future clang changes this, the sweep says so. +**What is left, and it is most of what the sweep was meant to settle:** -`-fno-sanitize=signed-integer-overflow` is the one exclusion, because wrapping is what this language's arithmetic means. -Nothing else is excluded. The flag does **not** force `-O0` the way `--debug` does; see below for why that earned its -keep. `--sanitize --debug` together works and gives `-O0` plus source lines in the report. +1. **UBSan sees no Flan code and no flag changes that.** Its checks are branches clang's C frontend emits inline, not a + pass, so shift UB (`(<< 1 32)`, see Sharp edges), alignment, and the f32→i32 cast on NaN or an infinity — the things + `floor-f32` guards by hand and nothing else does — are unreached. Either `Emit` grows those checks behind the flag, + which is a compiler feature of the same shape the bounds checks already have, or they belong to the checker. Not + decided. `test_sanitize` pins the current answer with a control that must *not* report, so a future clang changing + this is a test failure rather than a discovery. +2. **Four named buffers got no evidence at all.** The 4K result cap, the dev registry overflow guard, + `SNAP_MAX`/`SNAP_NAMES` and `condition_name[128]` are on the daemon and agent paths, which need a socket and are not + in the corpus. Their guards were read and are correct; that is reading, not testing. `escaped[ESCAPE_MAX]` is the one + that *is* covered, because `println.flan` drives a 1100-character string through it on purpose — 1019 bytes out + against a worst case of 1021 into 1024. `scratch[SCRATCH]` never sees more than 20 characters of 64. +3. **Valgrind over the headless corpus, not done.** ASan does not see uninitialised reads, which is where `zeroed` and + struct padding live. MSan is out: it needs every dependency instrumented and raylib settles that. -**The checked sweep is clean: 28 programs, no ASan report, no UBSan report, no divergence from the unsanitized run.** -What that does and does not prove: - -- It **does** cover `escaped[ESCAPE_MAX]` at its boundary. `println.flan` prints a 1100-character string inside a struct - on purpose; the escaped output is 1019 bytes against a hand-verified worst case of 1021 into 1024. That buffer is - genuinely exercised. -- It says **nothing** about `scratch[SCRATCH]`, whose longest reachable output is 20 characters (`%lld`) into 64. -- It says **nothing at all** about the 4K result cap, the dev registry overflow guard, `SNAP_MAX`/`SNAP_NAMES` or - `condition_name[128]`. Those are on the dev and agent paths, which need a daemon and a socket and are not in the - sweep's corpus. They were read and the guards are correct; that is reading, not evidence. - -**Two defects, both found by reading under the sanitizer rather than by the sanitizer, both fixed.** - -- `flan_bytes_to_i64` and `flan_bytes_to_f64` clamped with `(size_t)n < sizeof buf - 1`, and a slice's length is signed: - `(slice s 2 1)` is −1, `(size_t)(-1)` is not less than 511, so the `memcpy` read 63 or 511 bytes out of a five-byte - string constant. Every other `(ptr, len)` entry point in the runtime already folded a negative length to zero, so this - was two exceptions and not a missing convention. A checked build traps on the reversed slice first, which is why it - took `--no-bounds-checks` to show. Regression case in `test_sanitize`. -- The three `snprintf` shims published `scratch` as a slice using snprintf's return, which is what it *would* have - written. No format here can reach 64, so it could not fire; it is clamped anyway, because the distance between "cannot - fire" and "hands out a length past the end of a static buffer" is one format string. - -**Left, deliberately.** `break_loop` prints the condition name with `"%.*s"` and a negative `namelen` would drop the -precision and read to a NUL that a Flan string does not have — compiler-emitted and not reachable from source, so it is -recorded rather than fixed. `flan_bytes_to_f64` silently parses only the first 511 bytes, which changes a value rather -than corrupting memory. - -**ASan with `--no-bounds-checks`, the variant that asks whether the checks are the only thing holding the line. They -mostly are.** Of `bounds.flan`'s six deliberate out-of-bounds cases ASan catches three: - -| case | what it does | ASan | -|---|---|---| -| `3`, `7` | read and write past a 3-element global | caught | -| `4` | slice `hi` past the end of a string constant | caught | -| `-1` | negative index into a global | **silent** — a global gets a right redzone and nothing on its left | -| `9` | read past the end of a string constant | **silent at -O2, caught at -O0** | -| `2` | reversed slice, negative length | silent — nothing is read at all | - -Three of six is an upper bound on ASan's cover, not a measured fraction of the risk: ASan sees out-of-*object* access, -not out-of-subobject, so a slice into the middle of a larger array can overrun its logical bounds without crossing a -redzone, and the `-1` case is one instance of that class. **ASan is not a substitute for the bounds checks.** - -Case `9` is why `--sanitize` does not force `-O0`. At `-O2` the access does not happen: an out-of-bounds `inbounds` -getelementptr into a constant is poison, LLVM folds the load away, and the program prints a wrong answer instead of -touching anything. Same family as `(<< 1 32)` compiling to a bare `retq` under Sharp edges. Running the sweep at both -levels is cheap and a divergence between them is itself the finding. - -**Still not done.** Valgrind over the headless corpus, for the uninitialised reads ASan cannot see — where `zeroed` and -struct padding live. MSan is out because it needs every dependency instrumented and raylib settles that. The reload path -is uninstrumented whatever the flag says: a redefinition module is built by `llc` and `ld`, not by clang, so nothing -puts a pass over it. +Two things the sweep structurally cannot cover: raylib and libm are uninstrumented, so the windowed examples are noise; +and a redefinition module is built by `llc` and `ld` rather than clang, so the reload path carries no instrumentation +whatever the flag says. ### Managed classes are planned. Do not start them. diff --git a/test/test_sanitize.ml b/test/test_sanitize.ml index a68ab28..cf384ab 100644 --- a/test/test_sanitize.ml +++ b/test/test_sanitize.ml @@ -198,9 +198,12 @@ let control ~expect_report ?(args = []) ~why name src = let unchecked_controls () = let reports = [ "3"; "7"; "4" ] in let silent = - [ "-1", "a negative index into a global: ASan gives a global a right \ - redzone and nothing on the left, so arr[-1] lands in whatever \ - is in front of it"; + [ "-1", "a negative index into a global. Not a property of the access: \ + ASan lays a global out as {data, redzone}, so an underflow is \ + caught when something redzoned precedes it and not when nothing \ + does — measured both ways, and here nothing does. Whether \ + reading before an array is seen at all is therefore up to what \ + the linker put in front of it"; "9", "at -O2 the load is folded away — an out-of-bounds inbounds GEP \ into a string constant is poison, so nothing is read and a wrong \ value is printed. Reported at -O0.";