method Max(a: int, b: int)
    returns (m: int)
  ensures m >= a && m >= b
  ensures m == a || m == b
{
  if a >= b { m := a; }
  else { m := b; }
}

predicate Sorted(s: seq<int>)
{
  forall i, j ::
    0 <= i < j < |s| ==>
      s[i] <= s[j]
}

method BinarySearch(a: array<int>,
    key: int)
    returns (index: int)
  requires Sorted(a[..])
  ensures 0 <= index ==>
    a[index] == key
  ensures index < 0 ==>
    forall k ::
      0 <= k < a.Length ==>
        a[k] != key
{
  var lo, hi := 0, a.Length;
  while lo < hi
    invariant 0 <= lo <= hi
  {
    var mid := (lo + hi) / 2;
    if a[mid] < key {
      lo := mid + 1;
    } else if key < a[mid] {
      hi := mid;
    } else {
      return mid;
    }
  }
  return -1;
}

lemma MaxCommutative(a: int, b: int)
  ensures Max(a, b) == Max(b, a)
{
}

fn verify(x: &State) -> bool {
    x.balance >= 0
        && x.locked <= x.balance
}

#[requires(n > 0)]
#[ensures(ret >= n)]
fn next_pow2(n: u64) -> u64 {
    let mut p = 1;
    while p < n {
        p <<= 1;
    }
    p
}

(declare-const x Int)
(declare-const y Int)
(assert (> x 0))
(assert (= (+ x y) 10))
(check-sat)
; sat
(get-model)
; (define-fun x () Int 3)
; (define-fun y () Int 7)

(assert (forall ((a Int) (b Int))
  (=> (and (> a 0) (> b 0))
      (> (+ a b) 0))))
(check-sat)
; unsat

impl Repair for Patch {
    fn verify(&self) -> Outcome {
        if self.tests_pass()
            && self.no_regression() {
            Outcome::Plausible
        } else {
            Outcome::Rejected
        }
    }
}

ChatAFL

Published: February 26, 2024

ChatAFL is a protocol fuzzer guided by large language models, developed for our NDSS 2024 paper by R. Meng, M. Mirchev, M. Böhme, and A. Roychoudhury. It uses LLMs to help the fuzzer understand protocol semantics and overcome state-machine coverage plateaus that defeat purely mutation-based fuzzers. See the publication for details.

Share on

Twitter Facebook LinkedIn

Martin Mirchev

Share on