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
        }
    }
}

Large Language Model guided Protocol Fuzzing

Published in NDSS 2024, 2024

This paper shows how large language models can guide protocol fuzzing to discover bugs in protocol implementations more effectively.

Recommended citation: R. Meng, M. Mirchev, M. Böhme, A. Roychoudhury. (2024). "Large Language Model guided Protocol Fuzzing." Network and Distributed System Security Symposium (NDSS).

Share on

Twitter Facebook LinkedIn

Martin Mirchev

Share on