trvon 5a4d27d60e

audit: loop 2 priorities — top 5 by ROI across all backends

- #1: wire binary BB Z3 encoder into scan pipeline (binary 50%→70%)
- #2: Juliet benchmark scoring (standardized recall/precision)
- #3: Rust OSS benchmark formalization (ripgrep 49 findings)
- #4: binary BB encoder pipeline wiring
- #5: watch mode + CI/CD integration

2026-05-29 21:25:10 -04:00

2.4 KiB

Raw Permalink Blame History

Loop 2 Priorities — Top 5 by ROI Across All Backends

Generated 2026-05-30. Cross-backend gap audit for next improvement iteration.

Top 5 by Impact/Effort

#	Gap	Backend	Impact	Effort	ROI
1	Z3 encoder: unify binary + source paths	Both	Binary DD: 50%→70%, Z3-proved binary findings	M	Highest
2	Juliet benchmark scoring (14 CWEs)	Source	Standardized recall/precision numbers	S	High
3	Rust OSS benchmark formalization	Rust	49 findings on ripgrep validated, formalize results	S	High
4	Binary BB encoder: wire into scan pipeline	Binary	Make binary_bb_encoder.cpp actually used in scans	S	High
5	Watch mode + CI/CD integration	Utility	Developer workflow improvement	S	Medium

Source Backend Status

Area	Coverage	Gap
Memory safety	8 detectors	Concurrency, race conditions
Injection/taint	2 detectors	SQL injection (shipped, not validated)
Code quality	4 new detectors	Deprecated API, weak crypto, format string
Performance	TU pre-filter, clone cache	Clone pre-filter, incremental scan
Z3 power	7 new Z3 detectors	Interprocedural, switch-case predicates

Binary Backend Status

Area	Baseline	Current	Target
Detection rate	3.7% (1/27)	~50% (70 findings)	70%
Detectors	0	2 (imports, strings)	5 (add xref, packed, BB-Z3)
Z3 support	None	BB encoder code exists	Wired into pipeline
IR	None	13 node kinds + tree	Used in detector pipeline

Rust Backend Status

Area	Baseline	Current
Product test	None	ripgrep: 49 findings
MIR analysis	None	MIR→Z3, summaries
Taint tracking	None	TaintOrigin + KnownSafePaths
Path predicates	None	&&/
FP reduction	100% on high-conf	ts_rs filter, augment_args filter

Recommended Loop 2 Implementation

Wire binary_bb_encoder into scan pipeline (S, binary 50%→55%)
Juliet benchmark scoring (S, source credibility)
Rust OSS formal benchmark (S, Rust credibility)
Watch mode (S, developer workflow)
Unify BinaryIR → Z3 with source encoder (M, binary 55%→70%)

Skip for now: interprocedural Z3 (L effort, M13 territory), concurrency detectors (beyond bounded model), switch-case path predicates (deferred per encoder audit).

2.4 KiB Raw Permalink Blame History