concolic_core/
lib.rs

1//! The architecture-neutral half of the concolic pipeline.
2//!
3//! Every item in this crate is stated over **traces, decisions and reports**.
4//! None names an instruction set, a register, a syscall number, or a cell
5//! layout. A frontend (SBF, x86-64, RV32IM, AArch64, ...) supplies:
6//!
7//! - a deterministic concrete reference run ([`Frontend::run`]),
8//! - a symbolic walk forced along a concrete branch log ([`Frontend::walk`]),
9//! - the flip query at one decision ([`Frontend::flip`]),
10//! - the symbolic surface's names in a model, and how to apply them
11//!   ([`Frontend::model_inputs`], [`Frontend::apply_inputs`]).
12//!
13//! Everything else - the frontier, the budgets, the verification predicate
14//! ("same sites, same directions, opposite at the flipped site"), the seven
15//! flip outcomes and the report - is fixed here. A path only counts when the
16//! frontend's own reference engine re-ran the model and agreed; a `Sat` model
17//! alone is never a witness.
18
19use std::collections::BTreeSet;
20
21use smtlite::{Model, Solution};
22
23/// One decision in a concrete trace: the site and the direction taken.
24///
25/// Operand **values** are deliberately absent. A changed input necessarily
26/// changes the operands of earlier comparisons that still go the same way, so a
27/// verification predicate that compared whole records would reject genuine
28/// flips. Sites and directions are the path.
29#[derive(Clone, Copy, Debug, PartialEq, Eq)]
30pub struct BranchRec {
31    /// The decision site (an address, in every frontend in this workspace).
32    pub site: u64,
33    /// Whether the branch was taken.
34    pub taken: bool,
35}
36
37/// What an attempted flip actually reached (§7.1 of the LACUNA account).
38#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord)]
39pub enum FlipOutcome {
40    /// The reference engine took the opposite side at the same site, with the
41    /// same prefix decisions, and the resulting path was new.
42    Verified,
43    /// The flip query was UNSAT under the path prefix: no input flips it here.
44    ProvenUnflippable,
45    /// The solver hit a bound before a verdict.
46    SolverUnknown,
47    /// No query was built (the walk could not replay the path or force the branch).
48    /// The default is the honest one: nothing was posed.
49    #[default]
50    NotPosed,
51    /// The flipped run failed at the engine level.
52    RunFailed,
53    /// The run completed but did not flip: the walker and the engine disagree.
54    Unconfirmed,
55    /// The run did take the opposite side, but the path was already seen.
56    AlreadyExplored,
57}
58
59/// One flip attempt, in decision order.
60#[derive(Clone, Debug, Default)]
61pub struct FlipRec {
62    /// The site the attempt was posed at.
63    pub at: u64,
64    /// The model's bindings over the symbolic surface (`in!...` names).
65    pub input: Vec<(String, u64)>,
66    /// Whether the reference engine verified the flip onto a new path.
67    pub verified: bool,
68    /// The structured outcome.
69    pub outcome: FlipOutcome,
70}
71
72/// A property query's outcome (the same algebra the SBF frontend uses).
73#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord)]
74pub enum PropertyOutcome {
75    /// Sat model, applied and re-run: the concrete readback violates the invariant.
76    Confirmed,
77    /// UNSAT under the path formula: no reaching input violates it.
78    Proven,
79    /// The solver hit a bound.
80    SolverUnknown,
81    /// No verification run was spent, or no query was built.
82    #[default]
83    NotPosed,
84    /// The verification run failed at the engine level.
85    RunFailed,
86    /// The model was applied, the run completed, and it did not violate.
87    Unreproduced,
88}
89
90/// One property-directed query on one walked path.
91#[derive(Clone, Debug, Default)]
92pub struct PropertyRec {
93    /// The assertion's label.
94    pub label: String,
95    /// What the query reached.
96    pub outcome: PropertyOutcome,
97    /// The observed operands on a confirmed violation.
98    pub violation: Option<(u64, u64)>,
99    /// The applied input, when a model was re-run.
100    pub input: Vec<(String, u64)>,
101}
102
103/// A sink reached on a walked path. The `kind` and argument names are the
104/// frontend's vocabulary; the ledger treats them as opaque labels.
105#[derive(Clone, Debug, Default)]
106pub struct SinkRec {
107    /// The call site.
108    pub site: u64,
109    /// The sink class (e.g. `cpi`, `transfer`, `ecall`, `syscall`).
110    pub kind: String,
111    /// Argument names and their concrete values on the walked path.
112    pub args: Vec<(String, u64)>,
113}
114
115/// The outcome of one concrete reference run.
116#[derive(Clone, Debug, Default)]
117pub struct RunResult {
118    /// The program's own return value, when it returned.
119    pub result: Option<i64>,
120    /// The trap text, when the run trapped instead of returning.
121    pub trapped: Option<String>,
122    /// The decisions the run made, in order.
123    pub log: Vec<BranchRec>,
124    /// Sinks reached.
125    pub sinks: Vec<SinkRec>,
126}
127
128/// The session report - the architecture-neutral subset of the engine report
129/// that the diagnosis layer reads.
130#[derive(Clone, Debug, Default)]
131pub struct Report {
132    /// The base run's result, when it returned.
133    pub result: Option<i64>,
134    /// Concrete runs spent.
135    pub runs: usize,
136    /// Flips the reference engine verified.
137    pub flips_verified: usize,
138    /// Sinks reached.
139    pub sinks: Vec<SinkRec>,
140    /// Property queries posed.
141    pub properties: Vec<PropertyRec>,
142    /// Every flip attempt.
143    pub flips: Vec<FlipRec>,
144    /// Gap notes, verbatim from the frontend.
145    pub gaps: Vec<String>,
146    /// The frontier emptied inside the budgets.
147    pub exhausted: bool,
148}
149
150/// The budgets a session ran under.
151#[derive(Clone, Copy, Debug, PartialEq, Eq)]
152pub struct Opts {
153    /// Hard cap on concrete runs.
154    pub max_runs: usize,
155    /// Hard cap on verified flips.
156    pub max_flips: usize,
157}
158
159impl Default for Opts {
160    fn default() -> Self {
161        Self {
162            max_runs: 64,
163            max_flips: 32,
164        }
165    }
166}
167
168/// What a frontend must provide for the loop to run.
169///
170/// The four obligations are exactly the soundness contract: `run` is
171/// deterministic, `walk` is a sound over-approximation of `run`'s prefix, and
172/// `model_inputs`/`apply_inputs` round-trip a model onto a runnable seed.
173pub trait Frontend {
174    /// The seed: the initial state, with its base concrete assignment.
175    type Seed: Clone;
176    /// The symbolic walk, owning whatever solver state the frontend keeps.
177    type Walk;
178
179    /// Run the reference engine concretely. Determinism is the frontend's
180    /// obligation; an engine-level failure is `Err`, not a trap.
181    fn run(&self, seed: &Self::Seed) -> Result<RunResult, String>;
182
183    /// Replay the concrete log symbolically. `None` when the walk cannot force
184    /// the path (a replay or lift limitation); the caller records that fact.
185    fn walk(&self, seed: &Self::Seed, log: &[BranchRec]) -> Option<Self::Walk>;
186
187    /// Pose the flip query at decision `i` of the forced walk.
188    fn flip(&self, walk: &mut Self::Walk, i: usize) -> Solution;
189
190    /// The decision site at index `i` of the walk.
191    fn site(&self, walk: &Self::Walk, i: usize) -> u64;
192
193    /// The model's bindings over the symbolic surface.
194    fn model_inputs(&self, model: &Model, walk: &Self::Walk) -> Vec<(String, u64)>;
195
196    /// Apply those bindings to a child seed.
197    fn apply_inputs(&self, seed: &Self::Seed, inputs: &[(String, u64)]) -> Self::Seed;
198
199    /// Gap notes the walk itself recorded (unsupported opcode, replay drift, ...).
200    fn walk_gaps(&self, _walk: &Self::Walk) -> Vec<String> {
201        Vec::new()
202    }
203
204    /// Sinks reached on the walked path.
205    fn walk_sinks(&self, _walk: &Self::Walk) -> Vec<SinkRec> {
206        Vec::new()
207    }
208}
209
210struct Pending<S> {
211    seed: S,
212    run: RunResult,
213}
214
215struct Attempt<S> {
216    rec: FlipRec,
217    verified: bool,
218    ran: bool,
219    gap: Option<String>,
220    child: Option<Pending<S>>,
221}
222
223/// Explore the frontend's entry point from `base` inside the budgets.
224///
225/// The loop is the DART/CUTE shape: run, replay the path symbolically, pose a
226/// flip query at every decision (deepest first), apply a model, re-run, verify.
227/// A verified flip pushes the child path onto the frontier; the frontier
228/// emptying inside the budgets sets `exhausted`.
229#[must_use]
230pub fn explore<F: Frontend>(frontend: &F, base: &F::Seed, opts: &Opts) -> Report {
231    let mut report = Report::default();
232    let mut seen: BTreeSet<Vec<bool>> = BTreeSet::new();
233
234    let first = match frontend.run(base) {
235        Ok(r) => r,
236        Err(e) => {
237            report.gaps.push(format!("run failed: {e}"));
238            return report;
239        }
240    };
241    report.runs = 1;
242    report.result = first.result;
243    let mut frontier = vec![Pending { seed: base.clone(), run: first }];
244
245    while let Some(item) = frontier.pop() {
246        if report.runs >= opts.max_runs || report.flips_verified >= opts.max_flips {
247            return report;
248        }
249        if let Some(t) = &item.run.trapped {
250            report.gaps.push(format!("run trapped: {t}"));
251        }
252        let path: Vec<bool> = item.run.log.iter().map(|b| b.taken).collect();
253        if !seen.insert(path) {
254            continue;
255        }
256        let Some(mut walk) = frontend.walk(&item.seed, &item.run.log) else {
257            report
258                .gaps
259                .push("walk could not replay the concrete path".to_string());
260            continue;
261        };
262        report.sinks.extend(frontend.walk_sinks(&walk));
263        report.gaps.extend(frontend.walk_gaps(&walk));
264
265        // Deepest decision first, with the budgets checked against what this
266        // round has already spent - the same exact-cap discipline the SBF
267        // engine records.
268        let (mut spent, mut flipped) = (0usize, 0usize);
269        let mut attempts = Vec::new();
270        for i in (0..item.run.log.len()).rev() {
271            if report.runs + spent >= opts.max_runs
272                || report.flips_verified + flipped >= opts.max_flips
273            {
274                break;
275            }
276            let a = attempt(frontend, &item.seed, &item.run.log, &mut walk, i, &seen);
277            spent += usize::from(a.ran);
278            flipped += usize::from(a.verified);
279            attempts.push(a);
280        }
281
282        for a in attempts {
283            report.runs += usize::from(a.ran);
284            if let Some(g) = a.gap {
285                report.gaps.push(g);
286            }
287            report.flips.push(a.rec);
288            if a.verified {
289                report.flips_verified += 1;
290                if let Some(child) = a.child {
291                    frontier.push(child);
292                }
293            }
294        }
295    }
296    report.exhausted = true;
297    report
298}
299
300fn attempt<F: Frontend>(
301    frontend: &F,
302    seed: &F::Seed,
303    log: &[BranchRec],
304    walk: &mut F::Walk,
305    i: usize,
306    seen: &BTreeSet<Vec<bool>>,
307) -> Attempt<F::Seed> {
308    let at = frontend.site(walk, i);
309    let solution = frontend.flip(walk, i);
310    let Solution::Sat(m) = &solution else {
311        let outcome = match solution {
312            Solution::Unsat => FlipOutcome::ProvenUnflippable,
313            Solution::Unknown => FlipOutcome::SolverUnknown,
314            _ => FlipOutcome::NotPosed,
315        };
316        let gap = (outcome == FlipOutcome::SolverUnknown)
317            .then(|| format!("solver Unknown at {at:#x}"));
318        return Attempt {
319            rec: FlipRec { at, input: Vec::new(), verified: false, outcome },
320            verified: false,
321            ran: false,
322            gap,
323            child: None,
324        };
325    };
326
327    let inputs = frontend.model_inputs(m, walk);
328    let child_seed = frontend.apply_inputs(seed, &inputs);
329    let child_run = match frontend.run(&child_seed) {
330        Ok(r) => r,
331        Err(_) => {
332            return Attempt {
333                rec: FlipRec {
334                    at,
335                    input: inputs,
336                    verified: false,
337                    outcome: FlipOutcome::RunFailed,
338                },
339                verified: false,
340                ran: true,
341                gap: None,
342                child: None,
343            };
344        }
345    };
346
347    // Verification: the SAME sites in the SAME directions up to decision `i`,
348    // and the opposite direction at `i`. Operand values are not compared.
349    let prefix_ok = child_run.log.len() > i
350        && child_run.log[..i]
351            .iter()
352            .zip(&log[..i])
353            .all(|(c, p)| c.site == p.site && c.taken == p.taken);
354    let flipped =
355        prefix_ok && child_run.log[i].site == log[i].site && child_run.log[i].taken != log[i].taken;
356
357    let child_path: Vec<bool> = child_run.log.iter().map(|b| b.taken).collect();
358    let verified = flipped && !seen.contains(&child_path);
359    let outcome = if verified {
360        FlipOutcome::Verified
361    } else if flipped {
362        FlipOutcome::AlreadyExplored
363    } else {
364        FlipOutcome::Unconfirmed
365    };
366
367    Attempt {
368        rec: FlipRec { at, input: inputs, verified, outcome },
369        verified,
370        ran: true,
371        gap: None,
372        child: verified.then_some(Pending { seed: child_seed, run: child_run }),
373    }
374}
375
376#[cfg(test)]
377mod tests {
378    use super::*;
379
380    /// A toy frontend: one symbolic byte `x`. The program branches on `x < 0x10`
381    /// at site 0x100, then on `x == 0x42` at site 0x200. It exists to prove the
382    /// loop and the verification predicate are independent of any real ISA.
383    struct Toy;
384
385    #[derive(Clone)]
386    struct Seed {
387        x: u8,
388    }
389
390    struct Walk {
391        solver: smtlite::Solver,
392        x: smtlite::Bv,
393        conds: Vec<smtlite::Bv>,
394        taken: Vec<bool>,
395        path: Vec<smtlite::Bv>,
396    }
397
398    impl Frontend for Toy {
399        type Seed = Seed;
400        type Walk = Walk;
401
402        fn run(&self, seed: &Self::Seed) -> Result<RunResult, String> {
403            let mut log = Vec::new();
404            let x = seed.x;
405            log.push(BranchRec { site: 0x100, taken: x < 0x10 });
406            if x < 0x10 {
407                log.push(BranchRec { site: 0x200, taken: x == 0x42 });
408            }
409            Ok(RunResult { result: Some(i64::from(x)), trapped: None, log, sinks: Vec::new() })
410        }
411
412        fn walk(&self, _seed: &Self::Seed, log: &[BranchRec]) -> Option<Self::Walk> {
413            let mut solver = smtlite::Solver::new();
414            let x = solver.var("in!x", 8);
415            let mut conds = Vec::new();
416            let mut taken = Vec::new();
417            let mut path = Vec::new();
418            for b in log {
419                let cond = match b.site {
420                    0x100 => x.ult(&smtlite::Bv::val(0x10, 8)),
421                    0x200 => x.eq(&smtlite::Bv::val(0x42, 8)),
422                    _ => return None,
423                };
424                path.push(if b.taken { cond.clone() } else { cond.not() });
425                conds.push(cond);
426                taken.push(b.taken);
427            }
428            Some(Walk { solver, x, conds, taken, path })
429        }
430
431        fn flip(&self, walk: &mut Self::Walk, i: usize) -> Solution {
432            // Q_i = Phi_i AND NOT g_i: the prefix held, the branch forced the
433            // other way. `g_i` is the direction the concrete run took.
434            let g_i = if walk.taken[i] {
435                walk.conds[i].not()
436            } else {
437                walk.conds[i].clone()
438            };
439            let mut assumptions = walk.path[..i].to_vec();
440            assumptions.push(g_i);
441            walk.solver.check_all(&assumptions)
442        }
443
444        fn site(&self, walk: &Self::Walk, i: usize) -> u64 {
445            let _ = walk;
446            [0x100, 0x200][i]
447        }
448
449        fn model_inputs(&self, model: &Model, _walk: &Self::Walk) -> Vec<(String, u64)> {
450            model.get("in!x").map(|v| vec![("in!x".to_string(), v)]).unwrap_or_default()
451        }
452
453        fn apply_inputs(&self, _seed: &Self::Seed, inputs: &[(String, u64)]) -> Self::Seed {
454            Seed { x: inputs.first().map_or(0, |(_, v)| *v as u8) }
455        }
456    }
457
458    #[test]
459    fn the_loop_verifies_a_real_flip_and_proves_the_unreachable_one() {
460        let r = explore(&Toy, &Seed { x: 0 }, &Opts { max_runs: 64, max_flips: 32 });
461        // Base path: 0x100 taken, 0x200 not taken. The attempt at 0x200 asks
462        // whether x < 0x10 AND x == 0x42 - UNSAT, a local negative. The
463        // attempt at 0x100 is satisfiable, applied and re-run, and the
464        // reference engine takes the other side: Verified. The child path's
465        // own flip lands back on the base path: AlreadyExplored.
466        assert_eq!(r.runs, 3, "flips={:?}", r.flips);
467        assert_eq!(r.flips_verified, 1, "flips={:?}", r.flips);
468        assert_eq!(
469            r.flips.iter().map(|f| (f.at, f.outcome)).collect::<Vec<_>>(),
470            vec![
471                (0x200, FlipOutcome::ProvenUnflippable),
472                (0x100, FlipOutcome::Verified),
473                (0x100, FlipOutcome::AlreadyExplored),
474            ]
475        );
476        assert!(r.exhausted);
477    }
478}
concolic_core/lib.rs

concolic_core/
lib.rs
