mirror of
https://github.com/elicpeter/nyx.git
synced 2026-06-09 19:45:13 +02:00
[pitboss] sweep after phase 26: 4 deferred items resolved
This commit is contained in:
parent
8a801953e2
commit
ea722dc9ca
8 changed files with 320 additions and 130 deletions
|
|
@ -163,7 +163,7 @@ impl ChainFinding {
|
|||
if verdict.status == VerifyStatus::Inconclusive {
|
||||
self.severity = self.severity.downgraded();
|
||||
let reason = match &verdict.inconclusive_reason {
|
||||
Some(r) => format!("composite reverification inconclusive: {r:?}"),
|
||||
Some(r) => format!("composite reverification inconclusive: {r}"),
|
||||
None => match verdict.detail.as_deref() {
|
||||
Some(d) if !d.is_empty() => {
|
||||
format!("composite reverification inconclusive: {d}")
|
||||
|
|
|
|||
|
|
@ -184,6 +184,37 @@ const _: () = assert!(
|
|||
drop it from IMPACT_LATTICE_COVERED or add a rule that consumes it",
|
||||
);
|
||||
|
||||
/// Precomputed standalone-rule table indexed by `Cap` bit position.
|
||||
///
|
||||
/// Built once at compile time from [`IMPACT_LATTICE`]. `Cap` is a
|
||||
/// `bitflags!` u32, so each cap occupies one bit position 0..32; the
|
||||
/// table stores the standalone [`ImpactCategory`] (if any) for that
|
||||
/// position. [`lookup_impact`] uses this to short-circuit its
|
||||
/// second-pass and third-pass walks in O(1).
|
||||
static STANDALONE_BY_BIT: [Option<ImpactCategory>; 32] = build_standalone_table();
|
||||
|
||||
const fn build_standalone_table() -> [Option<ImpactCategory>; 32] {
|
||||
let mut table = [None; 32];
|
||||
let mut i = 0;
|
||||
while i < IMPACT_LATTICE.len() {
|
||||
let rule = IMPACT_LATTICE[i];
|
||||
if rule.adjacent_cap.is_none() {
|
||||
let bit = rule.source_cap.bits().trailing_zeros() as usize;
|
||||
table[bit] = Some(rule.result);
|
||||
}
|
||||
i += 1;
|
||||
}
|
||||
table
|
||||
}
|
||||
|
||||
fn standalone_lookup(cap: Cap) -> Option<ImpactCategory> {
|
||||
let bits = cap.bits();
|
||||
if bits == 0 || bits.count_ones() != 1 {
|
||||
return None;
|
||||
}
|
||||
STANDALONE_BY_BIT[bits.trailing_zeros() as usize]
|
||||
}
|
||||
|
||||
/// Look up an [`ImpactCategory`] for a (source, adjacent) cap pair.
|
||||
///
|
||||
/// `adjacent` is `None` when the caller has not yet found a partner
|
||||
|
|
@ -192,6 +223,12 @@ const _: () = assert!(
|
|||
/// Phase 25's path search calls this once per candidate path with the
|
||||
/// path's primary and secondary caps; multiple cap matches choose the
|
||||
/// first rule in [`IMPACT_LATTICE`] order (specific before fallback).
|
||||
///
|
||||
/// The standalone-rule walks (second + third pass) are O(1) via
|
||||
/// [`STANDALONE_BY_BIT`]. The two-cap walk (first pass) stays linear
|
||||
/// because the 2-cap subset is small (today: three rules); promote
|
||||
/// to a sorted-pair binary search if the lattice grows past ~16
|
||||
/// pair-rules.
|
||||
pub fn lookup_impact(source: Cap, adjacent: Option<Cap>) -> Option<ImpactCategory> {
|
||||
// First pass: exact source + matching adjacency (or both ways).
|
||||
if let Some(adj) = adjacent {
|
||||
|
|
@ -205,20 +242,16 @@ pub fn lookup_impact(source: Cap, adjacent: Option<Cap>) -> Option<ImpactCategor
|
|||
}
|
||||
}
|
||||
}
|
||||
// Second pass: standalone rule on source_cap.
|
||||
for rule in IMPACT_LATTICE {
|
||||
if rule.adjacent_cap.is_none() && rule.source_cap == source {
|
||||
return Some(rule.result);
|
||||
}
|
||||
// Second pass: standalone rule on source_cap (O(1) table lookup).
|
||||
if let Some(cat) = standalone_lookup(source) {
|
||||
return Some(cat);
|
||||
}
|
||||
// Third pass: if `adjacent` is given but the pair didn't hit,
|
||||
// try the standalone rule on adjacent_cap so a CODE_EXEC + UNRELATED
|
||||
// pair still reaches `Rce`.
|
||||
if let Some(adj) = adjacent {
|
||||
for rule in IMPACT_LATTICE {
|
||||
if rule.adjacent_cap.is_none() && rule.source_cap == adj {
|
||||
return Some(rule.result);
|
||||
}
|
||||
if let Some(cat) = standalone_lookup(adj) {
|
||||
return Some(cat);
|
||||
}
|
||||
}
|
||||
None
|
||||
|
|
|
|||
|
|
@ -135,8 +135,5 @@ impl ChainGraph {
|
|||
/// Phase 25's path-search code calls this as a fast-path before
|
||||
/// consulting the full [`IMPACT_LATTICE`].
|
||||
pub fn standalone_impact(cap: Cap) -> Option<ImpactCategory> {
|
||||
IMPACT_LATTICE
|
||||
.iter()
|
||||
.find(|rule| rule.source_cap == cap && rule.adjacent_cap.is_none())
|
||||
.map(|rule| rule.result)
|
||||
lookup_impact(cap, None)
|
||||
}
|
||||
|
|
|
|||
|
|
@ -217,9 +217,25 @@ fn compose_chain(
|
|||
let sink_cap = sole_cap(sink.cap_bits)?;
|
||||
let (impact, member_impacts) =
|
||||
resolve_impact(&path, sink_cap, entry, local_listener_present)?;
|
||||
Some(build_chain(entry, sink, &path, impact, &member_impacts))
|
||||
let mut chain = build_chain(entry, sink, &path, impact, &member_impacts);
|
||||
// SSRF + LocalListener refinement (Phase 24 deferred close): when
|
||||
// the implied impact is `InternalNetworkAccess` AND the SurfaceMap
|
||||
// exposes a loopback listener, the chain is more concrete than the
|
||||
// bare lattice match — lift the score so it ranks above SSRF chains
|
||||
// without a corroborating in-process target.
|
||||
if impact == ImpactCategory::InternalNetworkAccess && local_listener_present {
|
||||
chain.score *= LOCAL_LISTENER_BOOST;
|
||||
}
|
||||
Some(chain)
|
||||
}
|
||||
|
||||
/// Score multiplier applied when an `InternalNetworkAccess` chain has
|
||||
/// a corroborating loopback listener in the SurfaceMap. Calibrated to
|
||||
/// lift the chain above an otherwise-identical SSRF chain that lacks
|
||||
/// the listener context, without overtaking strictly more severe
|
||||
/// categories.
|
||||
const LOCAL_LISTENER_BOOST: f64 = 1.5;
|
||||
|
||||
/// Pick the lowest-bit single [`Cap`] from `bits`, or `None` when no
|
||||
/// bit is set. Sinks in the SurfaceMap may carry multi-bit
|
||||
/// `cap_bits`; the DFS terminates against the lowest single bit so
|
||||
|
|
@ -557,6 +573,61 @@ mod tests {
|
|||
}
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn ssrf_with_local_listener_scores_higher_than_without() {
|
||||
use crate::surface::{DataStore, DataStoreKind};
|
||||
let edge = || -> ChainEdge {
|
||||
edge_with(
|
||||
"app.py",
|
||||
10,
|
||||
"taint-ssrf",
|
||||
Cap::SSRF,
|
||||
"/fetch",
|
||||
HttpMethod::POST,
|
||||
Feasibility::Confirmed,
|
||||
)
|
||||
};
|
||||
let mut surface_no_listener = SurfaceMap::new();
|
||||
surface_no_listener.nodes.push(entry("app.py", "/fetch", false));
|
||||
surface_no_listener
|
||||
.nodes
|
||||
.push(sink("app.py", 20, "requests.get", Cap::SSRF));
|
||||
let baseline = find_chains(
|
||||
&[edge()],
|
||||
&surface_no_listener,
|
||||
ChainSearchConfig {
|
||||
max_depth: 4,
|
||||
min_score: 0.0,
|
||||
},
|
||||
);
|
||||
assert_eq!(baseline.len(), 1);
|
||||
assert_eq!(baseline[0].implied_impact, ImpactCategory::InternalNetworkAccess);
|
||||
|
||||
let mut surface_with_listener = surface_no_listener.clone();
|
||||
surface_with_listener
|
||||
.nodes
|
||||
.push(SurfaceNode::DataStore(DataStore {
|
||||
location: loc("app.py", 5),
|
||||
kind: DataStoreKind::KeyValue,
|
||||
label: "redis://127.0.0.1:6379".into(),
|
||||
}));
|
||||
let boosted = find_chains(
|
||||
&[edge()],
|
||||
&surface_with_listener,
|
||||
ChainSearchConfig {
|
||||
max_depth: 4,
|
||||
min_score: 0.0,
|
||||
},
|
||||
);
|
||||
assert_eq!(boosted.len(), 1);
|
||||
assert_eq!(boosted[0].implied_impact, ImpactCategory::InternalNetworkAccess);
|
||||
let ratio = boosted[0].score / baseline[0].score;
|
||||
assert!(
|
||||
(ratio - LOCAL_LISTENER_BOOST).abs() < 1e-9,
|
||||
"expected ×{LOCAL_LISTENER_BOOST} boost, got ratio={ratio}"
|
||||
);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn score_threshold_drops_low_score_chains() {
|
||||
let mut surface = SurfaceMap::new();
|
||||
|
|
|
|||
|
|
@ -328,6 +328,68 @@ pub enum InconclusiveReason {
|
|||
},
|
||||
}
|
||||
|
||||
impl fmt::Display for InconclusiveReason {
|
||||
/// Human-readable phrasing per variant. Used by callers that splice
|
||||
/// the typed reason into a user-facing string (e.g. the
|
||||
/// `reverify_reason` field on a chain finding). Consumers that need
|
||||
/// structured access should read the enum variant directly via
|
||||
/// `VerifyResult::inconclusive_reason`.
|
||||
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||
match self {
|
||||
Self::OracleCollisionSuspected => {
|
||||
f.write_str("oracle collision suspected (marker matched without sink reach)")
|
||||
}
|
||||
Self::NonReproducible => f.write_str("repro artifact could not be written"),
|
||||
Self::BuildFailed => f.write_str("harness build failed after retries"),
|
||||
Self::SandboxError => f.write_str("sandbox error"),
|
||||
Self::SpecDerivationFailed { tried, hint } => {
|
||||
f.write_str("spec derivation failed (tried: ")?;
|
||||
for (i, s) in tried.iter().enumerate() {
|
||||
if i > 0 {
|
||||
f.write_str(", ")?;
|
||||
}
|
||||
write!(f, "{s}")?;
|
||||
}
|
||||
write!(f, "; hint: {hint})")
|
||||
}
|
||||
Self::EntryKindUnsupported {
|
||||
lang,
|
||||
attempted,
|
||||
supported,
|
||||
hint,
|
||||
} => {
|
||||
write!(
|
||||
f,
|
||||
"entry kind {attempted:?} unsupported for {lang:?} (supported: "
|
||||
)?;
|
||||
for (i, k) in supported.iter().enumerate() {
|
||||
if i > 0 {
|
||||
f.write_str(", ")?;
|
||||
}
|
||||
write!(f, "{k:?}")?;
|
||||
}
|
||||
write!(f, "; hint: {hint})")
|
||||
}
|
||||
Self::NoBenignControl => {
|
||||
f.write_str("no benign control payload available for differential confirmation")
|
||||
}
|
||||
Self::ReversedDifferential => f.write_str(
|
||||
"reversed differential (benign payload fired, vulnerable payload did not)",
|
||||
),
|
||||
Self::UnrelatedCrash => {
|
||||
f.write_str("harness crashed outside the instrumented sink")
|
||||
}
|
||||
Self::BackendInsufficient {
|
||||
backend,
|
||||
oracle_kind,
|
||||
} => write!(
|
||||
f,
|
||||
"{backend} backend cannot enforce isolation for {oracle_kind} oracle"
|
||||
),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// High-level outcome of a dynamic verification attempt.
|
||||
///
|
||||
/// Serializes as PascalCase (`"Confirmed"`, `"NotConfirmed"`, etc.).
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue