Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
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
29 changes: 27 additions & 2 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions doc/src/SUMMARY.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
- [Snapshot Fuzzing](./design/snapshot-fuzzing.md)
- [Scenarios](./design/scenarios.md)
- [Intermediate Representation](./design/ir.md)
- [Assertions](./design/assertions.md)

# Usage

Expand Down
71 changes: 71 additions & 0 deletions doc/src/design/assertions.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
# Assertions

Fuzzamoto implements a feedback-guided assertion system inspired by
[Antithesis's sometimes
assertions](https://antithesis.com/docs/best_practices/sometimes_assertions/),
designed to both validate program correctness and guide fuzzing toward
interesting execution states.

The assertion system is only available when fuzzing with
[`fuzzamoto-libafl`](../usage/libafl.md).
Comment on lines +1 to +10
Copy link

@maflcko maflcko Dec 1, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The docs you link to are a bit vague around "sometimes assertions" being able to fail. Also, in the current implementation they are not able to fail, even if the fuzzing completes?

I am thinking, it could make sense to have both:

  • A macro to guide the fuzz engine to mark a condition as interesting and provide the fuzz engine with some kind of distance to reach it. Maybe this could be called reachability_goal(...) (or coverage_goal(...))
  • A macro to ensure different interesting "leaf" coverage is hit when iterating over a pre-generated, static set of (minimized) fuzz inputs in one folder. Maybe this could be called reachability_assert(...) (or coverage_assert(...)).

Such "reachability asserts" could help to more reliably trigger major coverage drops (google/oss-fuzz#11398). Not sure if this is in-scope for fuzzamoto, but I wanted to mention it, because it seems interesting in the greater fuzzing scope.

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The docs you link to are a bit vague around "sometimes assertions" being able to fail.

The way I understand it, failure for these assertions is defined as "over all tests we ran, the condition was never true", so in the context here, the following assertion would fail if none of the generated testcases ever managed to submit a valid transaction to the mempool.

assert_sometimes!(cond: mempool_size > 0, "Mempool is not empty");

This means that a failed assertion might flip to being satisfied over time as the fuzzing potentially discovers the right input. And in the other direction, a satisfied assertion might flip into failure if for some reason the coverage/state can no longer be reached.

Also, in the current implementation they are not able to fail, even if the fuzzing completes?

Yea in my implementation the sometimes assertions don't fail in a normal sense, but their status for a specific campaign can be inspected by looking at the assertion.txt file that is generated, e.g.:

✗ Sometimes gt(127, 1000): Mempool may contain more than 1000 txs
✓ Always cond(true): One active tip must exist
✓ Always lt(960096, 5000000): Mempool usage does not exceed the maximum
✓ Always lte(525000000000, 2100000000000000): Coin supply is within expected limits
✓ Sometimes cond(true): Block tip may change
✓ Sometimes cond(true): Mempool is not empty
✓ Sometimes cond(true): Node under test should send addr messages

I think I'll export the assertion "results" in a machine readable way, such that surrounding infrastructure can keep track and report issues based on them (e.g. coverage drops). Maybe also add some stats about the assertions to the stdout fuzzer output.

Such "reachability asserts" could help to more reliably trigger

I'll think about your suggested macros but I feel like the macros I have now could already satisfy those needs?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think I'll export the assertion "results" in a machine readable way, such that surrounding infrastructure can keep track and report issues based on them (e.g. coverage drops). Maybe also add some stats about the assertions to the stdout fuzzer output.

Such "reachability asserts" could help to more reliably trigger

I'll think about your suggested macros but I feel like the macros I have now could already satisfy those needs?

Yes, if your macro is designed so that surrounding infra decides how to treat a coverage miss, then both needs (explicitly assert on coverage, or just set a silent coverage goal) are satisfied. The only difference is that one approach puts the treatment of coverage misses in the source code directly, the other approach puts the treatment in the surrounding infra.

I guess a third option could also be to keep a single macro and set an env var to denote how the macro should behave: COVERAGE_ASSERT=0/1.

But all of this can trivially be implemented later and any approach looks good to me.


## Sometimes Assertions

Sometimes assertions express properties that should be satisfied *sometimes*
during fuzzing, rather than always. They serve two critical purposes during
fuzzing campaigns:

- **Detect reachability and verify coverage** - When assertions fire, they
confirm interesting program states are being reached. When they never fire,
it reveals either that the program state is unreachable (potentially
indicating a bug) or that the fuzzer isn't effective enough to reach it.
- **Guide exploration** - The fuzzer actively uses these assertions as
objectives, directing exploration toward satisfying them through
distance-based feedback.

Example usage:

```rust
assert_sometimes!(cond: mempool_size > 0, "Mempool is not empty");
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

q: where is the macro used? in the scenario?

Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It can be used in any code that runs inside the vm (scenario, oracles, targets, ...)

assert_sometimes!(gt: reorg_depth, 16, "Reorgs deeper than 16 blocks may occur");
```

Compared to traditional aggregate source code coverage reports, sometimes
assertions provide additional insights into the explored state space. For
example, a coverage report would tell us that a chain reorganization occured
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nit: occurred

but it would not inform us about the depth of those reorganizations.

## Always Assertions

Always assertions express invariants that must hold true at all times. They
detect violations of critical program properties:

```rust
assert_always!(lt: mempool_usage, max_mempool, "Mempool usage does not exceed the maximum");
assert_always!(lte: total_supply, 21_000_000, "Coin supply is within expected limits");
```

## Supported Assertion Types

Both `assert_sometimes!` and `assert_always!` support five variants:

- `cond: <bool>, <msg>` - Boolean condition
- `lt: <a>, <b>, <msg>` - Less than (a < b)
- `lte: <a>, <b>, <msg>` - Less than or equal (a ≤ b)
- `gt: <a>, <b>, <msg>` - Greater than (a > b)
- `gte: <a>, <b>, <msg>` - Greater than or equal (a ≥ b)

## Assertions as Feedback for Guiding Fuzzing

Unlike traditional assertions that simply pass or fail, Fuzzamoto assertions
calculate a *distance* metric that guides the fuzzer. A distance of 0 means the
assertion is satisfied, while a distance greater than 0 indicates how far the
current execution is from satisfying the assertion. For example, with
`assert_sometimes!(gt: value, 100, "...")`, if `value = 150` the distance is 0
(satisfied), but if `value = 95` the distance is 6 (need to increase by 6).

This distance metric is integrated with LibAFL's feedback mechanism. The fuzzer
tracks when assertions are triggered, favors inputs that reduce the distance to
unsatisfied assertions, and discovers inputs that reach interesting states
(sometimes assertions) or violate always assertions.

204 changes: 204 additions & 0 deletions fuzzamoto-libafl/src/feedbacks/assertions.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,204 @@
use std::borrow::Cow;
use std::collections::HashMap;
use std::fmt::Debug;
use std::fs::OpenOptions;
use std::path::PathBuf;
use std::time::{Duration, Instant};

use libafl::HasMetadata;
use libafl::corpus::Testcase;
use libafl::observers::StdOutObserver;
use libafl_bolts::tuples::{Handle, Handled, MatchName, MatchNameRef};
use libafl_bolts::{Error, Named, impl_serdeany};

use libafl::{
executors::ExitKind,
feedbacks::{Feedback, StateInitializer},
};

use fuzzamoto::assertions::{AssertionScope, write_assertions};

/// Parse assertions from raw stdout bytes.
///
/// This extracts all `AssertionScope` entries from the stdout output of a
/// fuzzamoto target execution.
pub fn parse_assertions_from_stdout(buffer: &[u8]) -> HashMap<String, AssertionScope> {
let stdout = String::from_utf8_lossy(buffer);
let mut assertions = HashMap::new();
for line in stdout.lines() {
let trimmed = line.trim().trim_matches(|c| c == '\0');
if let Ok(fuzzamoto::StdoutMessage::Assertion(data)) =
serde_json::from_str::<fuzzamoto::StdoutMessage>(trimmed)
{
use base64::prelude::{BASE64_STANDARD, Engine};
if let Ok(decoded) = BASE64_STANDARD.decode(&data)
&& let Ok(json) = String::from_utf8(decoded)
&& let Ok(assertion) = serde_json::from_str::<AssertionScope>(&json)
{
assertions.insert(assertion.message(), assertion);
}
}
}
assertions
}

#[derive(serde::Serialize, serde::Deserialize, Debug, Clone)]
pub struct AssertionFeedback {
assertions: HashMap<String, AssertionScope>,
o_ref: Handle<StdOutObserver>,

last_assertion_updates: Vec<String>,

#[serde(skip)]
last_update: Option<Instant>,
#[serde(skip)]
update_interval: Option<Duration>,
#[serde(skip)]
output_file: Option<PathBuf>,

// Only consider always assertions
only_always_assertions: bool,
}

impl AssertionFeedback {
fn evaluate_assertion(&mut self, new: AssertionScope) -> bool {
if self.only_always_assertions && matches!(new, AssertionScope::Sometimes(_, _)) {
return false;
}

let previous = self.assertions.get(&new.message());

let result = match (previous, &new) {
(None, new) => new.evaluate() || !self.only_always_assertions,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why is !self.only_always_assertions needed? Is it so that a Sometimes entry can be put into self.assertions and then later evaluate_assertion calls get closer in distance?

(Some(prev), new) => {
(!prev.evaluate() && new.evaluate()) || (prev.distance() > new.distance())
}
};

if result {
log::debug!("{previous:?} -> {new:?}");
self.last_assertion_updates.push(new.message());
self.assertions.insert(new.message(), new);
}

result
}
}

impl<S> StateInitializer<S> for AssertionFeedback {}

impl<EM, I, OT, S> Feedback<EM, I, OT, S> for AssertionFeedback
where
OT: MatchName,
{
fn is_interesting(
&mut self,
_state: &mut S,
_manager: &mut EM,
_input: &I,
observers: &OT,
_exit_kind: &ExitKind,
) -> Result<bool, Error> {
self.last_assertion_updates.clear();

let observer = observers
.get(&self.o_ref)
.ok_or(Error::illegal_state("StdOutObserver is missing"))?;
let buffer = observer
.output
.as_ref()
.ok_or(Error::illegal_state("StdOutObserver has no stdout"))?;

let parsed = parse_assertions_from_stdout(buffer);
let mut interesting = false;
for (_, assertion) in parsed {
interesting |= self.evaluate_assertion(assertion);
}

let now = Instant::now();
if !self.only_always_assertions
&& let Some(output_path) = self.output_file.as_ref()
&& now > self.last_update.unwrap() + self.update_interval.unwrap()
{
self.last_update = Some(now);

let mut output_file = OpenOptions::new()
.create(true)
.write(true)
.truncate(true)
.open(output_path)
.map_err(|e| {
log::warn!("Writing assertions to file: {e:?}");
libafl::Error::unknown(format!("Failed to open output file: {e}"))
})?;
write_assertions(&mut output_file, &self.assertions).map_err(|e| {
libafl::Error::unknown(format!("Failed to wirte to output file: {e}"))
})?;
}

Ok(interesting)
}

fn append_metadata(
&mut self,
_state: &mut S,
_manager: &mut EM,
_observers: &OT,
testcase: &mut Testcase<I>,
) -> Result<(), Error> {
let mut assertions = HashMap::new();
for msg in &self.last_assertion_updates {
if let Some(assertion) = self.assertions.get(msg) {
assertions.insert(msg.clone(), assertion.clone());
}
}

testcase.add_metadata(AssertionMetadata { assertions });

Ok(())
}
}

#[derive(serde::Serialize, serde::Deserialize, Debug, Clone)]
pub struct AssertionMetadata {
pub assertions: HashMap<String, AssertionScope>,
}

impl_serdeany!(AssertionMetadata);

impl Named for AssertionFeedback {
#[inline]
fn name(&self) -> &Cow<'static, str> {
self.o_ref.name()
}
}

impl AssertionFeedback {
/// Creates a new [`AssertionFeedback`].
#[must_use]
pub fn new(observer: &StdOutObserver, output_file: PathBuf) -> Self {
let interval = Duration::from_secs(30);
Self {
o_ref: observer.handle(),
assertions: HashMap::new(),
last_assertion_updates: Vec::new(),
output_file: Some(output_file),

last_update: Some(Instant::now().checked_sub(interval * 2).unwrap()),
update_interval: Some(interval),

only_always_assertions: false,
}
}
pub fn new_only_always(observer: &StdOutObserver) -> Self {
Self {
o_ref: observer.handle(),
assertions: HashMap::new(),
last_assertion_updates: Vec::new(),
output_file: None,
last_update: None,
update_interval: None,
only_always_assertions: true,
}
}
}
2 changes: 2 additions & 0 deletions fuzzamoto-libafl/src/feedbacks/mod.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
pub mod assertions;

use regex::bytes::Regex;
use std::{borrow::Cow, cell::RefCell, fmt::Debug, rc::Rc};

Expand Down
Loading