Skip to content

refactor(prover): remove legacy unused reachability constraints #2441

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
eviehoward wants to merge 3 commits into
base: main
Choose a base branch
from
+1 −147
Open

refactor(prover): remove legacy unused reachability constraints #2441

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
27d24f0
refactor(prover): remove legacy unused reachability constraints
eviehoward Jul 22, 2026
4873bbc
refactor(prover): remove dead write-capability helpers from binary re…
eviehoward Jul 22, 2026
0009e7c
docs(prover): remove stale write-bypass mention from module doc comment
eviehoward Jul 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion crates/openshell-prover/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
//!
//! Encodes sandbox policies, binary capabilities, and credential scopes as Z3
//! SMT constraints, then checks reachability queries to detect data exfiltration
//! paths and write-bypass violations.
//! paths.

pub mod accepted_risks;
pub mod credentials;
Expand Down
114 changes: 0 additions & 114 deletions crates/openshell-prover/src/model.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,14 +45,8 @@ pub struct ReachabilityModel {
l7_enforced: HashMap<String, Bool>,
l7_allows_write: HashMap<String, Bool>,
binary_bypasses_l7: HashMap<String, Bool>,
binary_can_write: HashMap<String, Bool>,
binary_can_exfil: HashMap<String, Bool>,
binary_can_construct_http: HashMap<String, Bool>,
credential_has_write: HashMap<String, Bool>,
#[allow(dead_code)]
credential_has_destructive: HashMap<String, Bool>,
#[allow(dead_code)]
filesystem_readable: HashMap<String, Bool>,
}

impl ReachabilityModel {
Expand All @@ -74,12 +68,8 @@ impl ReachabilityModel {
l7_enforced: HashMap::new(),
l7_allows_write: HashMap::new(),
binary_bypasses_l7: HashMap::new(),
binary_can_write: HashMap::new(),
binary_can_exfil: HashMap::new(),
binary_can_construct_http: HashMap::new(),
credential_has_write: HashMap::new(),
credential_has_destructive: HashMap::new(),
filesystem_readable: HashMap::new(),
};
model.build();
model
Expand All @@ -91,8 +81,6 @@ impl ReachabilityModel {
self.encode_policy_allows();
self.encode_l7_enforcement();
self.encode_binary_capabilities();
self.encode_credentials();
self.encode_filesystem();
}

fn index_endpoints(&mut self) {
Expand Down Expand Up @@ -198,14 +186,6 @@ impl ReachabilityModel {
}
self.binary_bypasses_l7.insert(bpath.clone(), bypass_var);

let write_var = Bool::new_const(format!("binary_can_write_{bpath}"));
if cap.can_write() {
self.solver.assert(&write_var);
} else {
self.solver.assert(&!write_var.clone());
}
self.binary_can_write.insert(bpath.clone(), write_var);

let exfil_var = Bool::new_const(format!("binary_can_exfil_{bpath}"));
if cap.can_exfiltrate {
self.solver.assert(&exfil_var);
Expand All @@ -225,106 +205,12 @@ impl ReachabilityModel {
}
}

fn encode_credentials(&mut self) {
let hosts: HashSet<String> = self.endpoints.iter().map(|e| e.host.clone()).collect();

for host in &hosts {
let creds = self.credentials.credentials_for_host(host);
let api = self.credentials.api_for_host(host);

let mut has_write = false;
let mut has_destructive = false;

for cred in &creds {
if let Some(api) = api {
if !api.write_actions_for_scopes(&cred.scopes).is_empty() {
has_write = true;
}
if !api.destructive_actions_for_scopes(&cred.scopes).is_empty() {
has_destructive = true;
}
} else if !cred.scopes.is_empty() {
has_write = true;
}
}

let cw_var = Bool::new_const(format!("credential_has_write_{host}"));
if has_write {
self.solver.assert(&cw_var);
} else {
self.solver.assert(&!cw_var.clone());
}
self.credential_has_write.insert(host.clone(), cw_var);

let destructive_var = Bool::new_const(format!("credential_has_destructive_{host}"));
if has_destructive {
self.solver.assert(&destructive_var);
} else {
self.solver.assert(&!destructive_var.clone());
}
self.credential_has_destructive
.insert(host.clone(), destructive_var);
}
}

fn encode_filesystem(&mut self) {
for path in self.policy.filesystem_policy.readable_paths() {
let var = Bool::new_const(format!("fs_readable_{path}"));
self.solver.assert(&var);
self.filesystem_readable.insert(path, var);
}
}

// --- Query helpers ---

fn false_val() -> Bool {
Bool::from_bool(false)
}

/// Build a Z3 expression for whether a binary can write to an endpoint.
pub fn can_write_to_endpoint(&self, bpath: &str, eid: &EndpointId) -> Bool {
let ek = eid.key();
let access_key = format!("{bpath}:{ek}");

let has_access = match self.policy_allows.get(&access_key) {
Some(v) => v.clone(),
None => return Self::false_val(),
};

let bypass = self
.binary_bypasses_l7
.get(bpath)
.cloned()
.unwrap_or_else(Self::false_val);
let l7_enforced = self
.l7_enforced
.get(&ek)
.cloned()
.unwrap_or_else(Self::false_val);
let l7_write = self
.l7_allows_write
.get(&ek)
.cloned()
.unwrap_or_else(Self::false_val);
let binary_write = self
.binary_can_write
.get(bpath)
.cloned()
.unwrap_or_else(Self::false_val);
let cred_write = self
.credential_has_write
.get(&eid.host)
.cloned()
.unwrap_or_else(Self::false_val);

Bool::and(&[
has_access,
binary_write,
Bool::or(&[!l7_enforced, l7_write, bypass]),
cred_write,
])
}

/// Build a Z3 expression for whether data can be exfiltrated via this path.
pub fn can_exfil_via_endpoint(&self, bpath: &str, eid: &EndpointId) -> Bool {
let ek = eid.key();
Expand Down
32 changes: 0 additions & 32 deletions crates/openshell-prover/src/registry.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,15 +100,6 @@ pub struct BinaryProtocol {
pub actions: Vec<BinaryAction>,
}

impl BinaryProtocol {
/// Whether any action in this protocol is a write or destructive action.
pub fn can_write(&self) -> bool {
self.actions
.iter()
.any(|a| matches!(a.action_type, ActionType::Write | ActionType::Destructive))
}
}

/// Capability descriptor for a single binary.
#[derive(Debug, Clone)]
pub struct BinaryCapability {
Expand All @@ -126,29 +117,6 @@ impl BinaryCapability {
pub fn bypasses_l7(&self) -> bool {
self.protocols.iter().any(|p| p.bypasses_l7)
}

/// Whether the binary can perform write actions.
pub fn can_write(&self) -> bool {
self.protocols.iter().any(BinaryProtocol::can_write) || self.can_construct_http
}

/// Short mechanisms by which this binary can write.
pub fn write_mechanisms(&self) -> Vec<String> {
let mut mechanisms = Vec::new();
for p in &self.protocols {
if p.can_write() {
for a in &p.actions {
if matches!(a.action_type, ActionType::Write | ActionType::Destructive) {
mechanisms.push(format!("{}: {}", p.name, a.name));
}
}
}
}
if self.can_construct_http {
mechanisms.push("arbitrary HTTP request construction".to_owned());
}
mechanisms
}
}

/// Registry of binary capability descriptors.
Expand Down
Loading