-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add the test case from our SOSP submission rebuttal (#162)
## What Changed? Adds a test case that substantiates our expectations wrt. the Plume policy quantifier does as expressed in the examples in the 2024 SOSP author response. ## Why Does It Need To? I made the test case, might as well use it. ## Checklist - [x] Above description has been filled out so that upon quash merge we have a good record of what changed. - [x] New functions, methods, types are documented. Old documentation is updated if necessary - [x] Documentation in Notion has been updated - [x] Tests for new behaviors are provided - [ ] New test suites (if any) ave been added to the CI tests (in `.github/workflows/rust.yml`) either as compiler test or integration test. *Or* justification for their omission from CI has been provided in this PR description.
- Loading branch information
1 parent
54bf07d
commit a4ca7a0
Showing
2 changed files
with
161 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,139 @@ | ||
use paralegal_flow::test_utils::{CtrlRef, FlowsTo, HasGraph, InlineTestBuilder, NodeRefs}; | ||
use paralegal_spdg::Identifier; | ||
|
||
fn policy(ctx: CtrlRef, quantifier: impl Fn(&NodeRefs, &NodeRefs) -> bool) -> Result<(), String> { | ||
let user_data_types = (&ctx).marked_types(Identifier::new_intern("user_data")); | ||
|
||
assert!(!user_data_types.is_empty()); | ||
|
||
let delete_sinks = ctx.marked(Identifier::new_intern("deletes")); | ||
assert!(!delete_sinks.is_empty()); | ||
for t in user_data_types { | ||
let srcs = ctx.nodes_for_type(t); | ||
if srcs.is_empty() { | ||
return Err(format!("No sources for {t:?}")); | ||
} | ||
if !quantifier(&srcs, &delete_sinks) { | ||
return Err(format!("failed for {t:?}")); | ||
} | ||
} | ||
Ok(()) | ||
} | ||
|
||
const SIMPLE_BUG: &str = stringify!( | ||
#[paralegal_flow::marker(deletes, arguments = [0])] | ||
fn delete<T>(t: T) {} | ||
|
||
#[paralegal_flow::marker(user_data)] | ||
struct User {} | ||
|
||
#[paralegal_flow::marker(user_data)] | ||
struct Post {} | ||
|
||
#[paralegal_flow::marker(user_data)] | ||
struct Comment {} | ||
|
||
fn main() { | ||
for post in vec![Post {}] { | ||
delete(post) | ||
} | ||
delete(User {}); | ||
} | ||
); | ||
|
||
const CORRECT: &str = stringify!( | ||
#[paralegal_flow::marker(deletes, arguments = [0])] | ||
fn delete<T>(t: T) {} | ||
|
||
#[paralegal_flow::marker(user_data)] | ||
struct User {} | ||
|
||
#[paralegal_flow::marker(user_data)] | ||
struct Post {} | ||
|
||
#[paralegal_flow::marker(user_data)] | ||
struct Comment {} | ||
|
||
fn main() { | ||
for post in vec![Post {}] { | ||
delete(post) | ||
} | ||
for comment in vec![Comment {}] { | ||
delete(comment) | ||
} | ||
delete(User {}); | ||
} | ||
); | ||
|
||
const FORALL_FAIL: &str = stringify!( | ||
#[paralegal_flow::marker(deletes, arguments = [0])] | ||
fn delete<T>(t: T) {} | ||
|
||
#[paralegal_flow::marker(user_data)] | ||
#[derive(PartialEq)] | ||
struct User {} | ||
|
||
fn main() { | ||
let current_user = User {}; | ||
let stored_users = vec![User {}]; | ||
if stored_users.contains(¤t_user) { | ||
delete(current_user); | ||
} | ||
} | ||
); | ||
|
||
const EXISTENTIAL_MISS: &str = stringify!( | ||
#[paralegal_flow::marker(deletes, arguments = [0])] | ||
fn delete<T>(t: T) {} | ||
|
||
#[paralegal_flow::marker(user_data)] | ||
struct Post {} | ||
|
||
fn main() { | ||
let first_half_of_user_posts = vec![Post {}]; | ||
let second_half_of_user_posts = vec![Post {}]; | ||
delete(first_half_of_user_posts); | ||
} | ||
); | ||
|
||
#[test] | ||
fn plume_policy_exists_quantifier() { | ||
let policy = |expect_success, msg| { | ||
move |ctrl: CtrlRef<'_>| { | ||
let result = policy(ctrl, |srcs, snks| srcs.flows_to_data(snks)); | ||
if expect_success { | ||
if let Err(e) = result { | ||
panic!("Failed {e} {msg}") | ||
} | ||
} else { | ||
assert!(result.is_err(), "Expected fail on {msg}"); | ||
} | ||
} | ||
}; | ||
InlineTestBuilder::new(SIMPLE_BUG).check(policy(false, "simple bug")); | ||
InlineTestBuilder::new(CORRECT).check(policy(true, "correct")); | ||
InlineTestBuilder::new(EXISTENTIAL_MISS).check(policy(true, "existential fail")); | ||
InlineTestBuilder::new(FORALL_FAIL).check(policy(true, "Forall false-positive")); | ||
} | ||
|
||
#[test] | ||
fn plume_policy_forall_quantifier() { | ||
let policy = |expect_success, msg| { | ||
move |ctrl: CtrlRef<'_>| { | ||
let result = policy(ctrl, |srcs, snks| { | ||
srcs.as_singles().all(|n| n.flows_to_data(snks)) | ||
}); | ||
if expect_success { | ||
if let Err(e) = result { | ||
panic!("Failed {e} {msg}") | ||
} | ||
} else { | ||
assert!(result.is_err(), "Expected fail {msg}"); | ||
} | ||
} | ||
}; | ||
InlineTestBuilder::new(SIMPLE_BUG).check(policy(false, "bug")); | ||
InlineTestBuilder::new(CORRECT).check(policy(true, "correct")); | ||
InlineTestBuilder::new(EXISTENTIAL_MISS).check(policy(false, "existential bug")); | ||
InlineTestBuilder::new(FORALL_FAIL).check(policy(false, "forall false-positive")); | ||
} |