diff --git a/.github/actions/with-docker/Dockerfile.fuzz b/.github/actions/with-docker/Dockerfile.fuzz new file mode 100644 index 0000000..21d546f --- /dev/null +++ b/.github/actions/with-docker/Dockerfile.fuzz @@ -0,0 +1,23 @@ +ARG K_VERSION=7.1.241 +ARG RUST_TOOLCHAIN=1.82.0 + +FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION} AS semantics + +WORKDIR /opt/imp-semantics +COPY examples/fuzzer/k-semantics . +RUN kompile --llvm-kompile-type c fuzz.k + +FROM rust:${RUST_TOOLCHAIN} + +COPY --from=semantics /opt/imp-semantics/fuzz-kompiled/interpreter.so /usr/lib +RUN apt-get update && apt-get install --yes build-essential binutils-dev libunwind-dev libblocksruntime-dev liblzma-dev +RUN cargo install honggfuzz + +ARG USER=user +ARG GROUP=$USER +ARG USER_ID=1000 +ARG GROUP_ID=$USER_ID + +RUN groupadd -g $GROUP_ID $GROUP && useradd -m -u $USER_ID -s /bin/sh -g $GROUP $USER + +USER $USER:$GROUP diff --git a/.github/actions/with-docker/action.yml b/.github/actions/with-docker/action.yml index 827f6ff..b4389d3 100644 --- a/.github/actions/with-docker/action.yml +++ b/.github/actions/with-docker/action.yml @@ -5,6 +5,10 @@ inputs: description: 'Docker container name to use' required: true type: string + dockerfile: + description: 'Dockerfile to use' + required: true + type: string runs: using: 'composite' steps: @@ -15,7 +19,7 @@ runs: CONTAINER_NAME=${{ inputs.container-name }} TAG=runtimeverificationinc/${CONTAINER_NAME} - DOCKERFILE=${{ github.action_path }}/Dockerfile + DOCKERFILE=${{ github.action_path }}/${{ inputs.dockerfile }} docker build . \ --file ${DOCKERFILE} \ diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index f3b39b3..041b8e9 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -16,9 +16,40 @@ jobs: uses: ./.github/actions/with-docker with: container-name: kframework-rs-${{ github.sha }} + dockerfile: Dockerfile - name: 'Build and test' run: docker exec -u user kframework-rs-${GITHUB_SHA} make - name: 'Tear down Docker' if: always() run: | docker stop --time=0 kframework-rs-${GITHUB_SHA} + + build-ffi-and-fuzz: + name: 'Build with the FFI and run the fuzzing example' + runs-on: [self-hosted, linux, normal] + steps: + - name: 'Check out code' + uses: actions/checkout@v4 + - name: 'Set up Docker' + uses: ./.github/actions/with-docker + with: + container-name: kframework-rs-fuzz-${{ github.sha }} + dockerfile: Dockerfile.fuzz + - name: 'Build and test' + run: | + export HFUZZ_RUN_ARGS="--verbose --logfile log.txt --run_time 60" + docker exec \ + --env HFUZZ_RUN_ARGS="${HFUZZ_RUN_ARGS}" \ + --workdir /home/user/examples/fuzzer \ + kframework-rs-fuzz-${GITHUB_SHA} \ + cargo hfuzz run fuzzer + echo "Final lines of hfuzz output:" + docker exec \ + --env HFUZZ_RUN_ARGS="${HFUZZ_RUN_ARGS}" \ + --workdir /home/user/examples/fuzzer \ + kframework-rs-fuzz-${GITHUB_SHA} \ + tail log.txt + - name: 'Tear down Docker' + if: always() + run: | + docker stop --time=0 kframework-rs-fuzz-${GITHUB_SHA} diff --git a/examples/fuzzer/Cargo.toml b/examples/fuzzer/Cargo.toml new file mode 100644 index 0000000..5c47adb --- /dev/null +++ b/examples/fuzzer/Cargo.toml @@ -0,0 +1,10 @@ +[package] +name = "fuzzer" +version = "0.1.0" +edition = "2021" + +[dependencies] +arbitrary = "1.4.1" +honggfuzz = "0.5.57" +kframework = { path = "../.." } +kframework_ffi = { path = "../../kframework_ffi" } diff --git a/examples/fuzzer/README.md b/examples/fuzzer/README.md new file mode 100644 index 0000000..2bc9a6a --- /dev/null +++ b/examples/fuzzer/README.md @@ -0,0 +1,29 @@ +# Imp fuzzing with kframework_ffi + +This is an example of a fuzzing target for a hashing function that uses the kllvm execution engine for the Imp semantics. + +## Requirements + +- An installation of the [kframework](https://github.com/runtimeverification/k) +- An installation of [rustup](https://rustup.rs/) +- Cargo installed [honggfuzz](https://github.com/rust-fuzz/honggfuzz-rs) + +NOTE: If you are using a `kup` installed version of K, then you are very likely to run into linking errors between the nix libraries and your installation of `rustup`. This should be able to get resolved by a proper derivation, but no such thing exists at the time of writing. + +## Setup + +``` +$ cd k-semantics +$ kompile --llvm-kompile-type c fuzz.k +$ export LD_LIBRARY_PATH=$(realpath fuzz-kompiled) +$ cd .. +$ cargo hfuzz run fuzzer +``` + +## Explanation + +The `FUZZ` semantics module extends Imp with an `Assert` statement which rewrites the entire configuration into a failing symbol when it doesn't pass. It also has a success symbol which it will rewrite the configuration to when execution is finished (ie. the cell is empty). + +There is an `init_fuzz` utility symbol which takes two integer parameters and then rewrites to an Imp program that performs a hash over those integers. The failure case for this program is arbitrarily if the hash ends up being a very low number. + +On the rust side, the fuzzing target uses the random input to construct this `init_fuzz` symbol and the initial configuration in the form of a kore string. Then it uses the foreign functions to build that configuration in kllvm's interned representation, execute it, and retrieve the resulting configuration as another kore string. Then it parses the kore string and checks for the failure or success case. diff --git a/examples/fuzzer/build.rs b/examples/fuzzer/build.rs new file mode 100644 index 0000000..9a67992 --- /dev/null +++ b/examples/fuzzer/build.rs @@ -0,0 +1,17 @@ +use std::env; + +fn main() { + // Link interpreter.so + println!("cargo:rustc-link-arg=-l:interpreter.so"); + + // Add the location of interpreter.so to your LD_LIBRARY_PATH variable + // You will also need this variable set when you run the program + match env::var_os("LD_LIBRARY_PATH") { + Some(paths) => { + for lib_path in env::split_paths(&paths) { + println!("cargo:rustc-link-search={}", lib_path.display()); + } + } + None => (), + }; +} diff --git a/examples/fuzzer/k-semantics/fuzz.k b/examples/fuzzer/k-semantics/fuzz.k new file mode 100644 index 0000000..7c26c21 --- /dev/null +++ b/examples/fuzzer/k-semantics/fuzz.k @@ -0,0 +1,45 @@ +requires "imp.k" + +module FUZZ + imports IMP + + configuration + + syntax Stmt ::= "Assert" "(" BExp ")" ";" [strict] + rule Assert( true ); => .K + + syntax Pgm ::= "init_fuzz" "(" Int "," Int ")" [symbol(init_fuzz)] + syntax TCell ::= "FUZZ_SUCCESS" [symbol(fuzz_success)] + | "FUZZ_FAILURE" [symbol(fuzz_failure)] + + syntax Id ::= "x" [token] + | "y" [token] + | "combined" [token] + | "salted" [token] + | "z" [token] + | "hash_val" [token] + + rule init_fuzz(X, Y) + => int x, y, combined, salted, z, hash_val; + + x = X; + y = Y; + + combined = x * 1000000 + y; + + salted = combined + 1; + + z = salted + 11400714819323198485; + z = (z ^ (z >> 30)) * 13787848793156543929; + z = (z ^ (z >> 27)) * 10723151780598845931; + z = z ^ (z >> 31); + + hash_val = z & 4294967295; + + Assert( !( hash_val <= 15000 ) ); + ... + + + rule .K ... => FUZZ_SUCCESS + rule Assert(false); ... ... => FUZZ_FAILURE +endmodule diff --git a/examples/fuzzer/k-semantics/imp.k b/examples/fuzzer/k-semantics/imp.k new file mode 100644 index 0000000..2e545b8 --- /dev/null +++ b/examples/fuzzer/k-semantics/imp.k @@ -0,0 +1,68 @@ +// Copyright (c) Runtime Verification, Inc. All Rights Reserved. + +module IMP-SYNTAX + imports DOMAINS-SYNTAX + syntax AExp ::= Int | Id + | "-" Int + | AExp "*" AExp [left, strict] + | AExp "^" AExp [left, strict] + | AExp ">>" AExp [left, strict] + | AExp "&" AExp [left, strict] + | "(" AExp ")" [bracket] + > AExp "+" AExp [left, strict] + syntax BExp ::= Bool + | AExp "<=" AExp [seqstrict] + | "!" BExp [strict] + | "(" BExp ")" [bracket] + > BExp "&&" BExp [left, strict(1)] + syntax Block ::= "{" "}" + | "{" Stmt "}" + syntax Stmt ::= Block + | Id "=" AExp ";" [strict(2)] + | "if" "(" BExp ")" + Block "else" Block [strict(1)] + | "while" "(" BExp ")" Block + > Stmt Stmt [left] + syntax Pgm ::= "int" Ids ";" Stmt + syntax Ids ::= List{Id,","} +endmodule + + +module IMP + imports IMP-SYNTAX + imports DOMAINS + syntax KResult ::= Int | Bool + + configuration + $PGM:Pgm + .Map + + +// AExp + rule X:Id => I ... ... X |-> I ... + rule I1 * I2 => I1 *Int I2 + rule I1 ^ I2 => I1 xorInt I2 + rule I1 >> I2 => I1 >>Int I2 + rule I1 & I2 => I1 &Int I2 + rule I1 + I2 => I1 +Int I2 + rule - I1 => 0 -Int I1 +// BExp + rule I1 <= I2 => I1 <=Int I2 + rule ! T => notBool T + rule true && B => B + rule false && _ => false +// Block + rule {} => .K + rule {S} => S +// Stmt + rule X = I:Int; => .K ... ... X |-> (_ => I) ... + rule S1:Stmt S2:Stmt => S1 ~> S2 + rule if (true) S else _ => S + rule if (false) _ else S => S + rule while (B) S => if (B) {S while (B) S} else {} +// Pgm + rule int (X,Xs => Xs);_ Rho:Map (.Map => X|->0) + requires notBool (X in keys(Rho)) + rule int .Ids; S => S + +endmodule diff --git a/examples/fuzzer/src/main.rs b/examples/fuzzer/src/main.rs new file mode 100644 index 0000000..9514343 --- /dev/null +++ b/examples/fuzzer/src/main.rs @@ -0,0 +1,103 @@ +use std::panic; + +use arbitrary::{Arbitrary, Unstructured}; +use honggfuzz::fuzz; +use kframework::kore::{App, Parser, Pattern, SymbolId}; +use kframework_ffi::kllvm; + +#[derive(Clone, Copy)] +struct FuzzInput { + field1: u32, + field2: u32, +} + +impl Arbitrary<'_> for FuzzInput { + fn arbitrary(u: &mut Unstructured<'_>) -> arbitrary::Result { + let field1 = u.int_in_range(0..=1000000)?; + let field2 = u.int_in_range(0..=1000000)?; + Ok(FuzzInput { field1, field2 }) + } +} + +/// Hardcoded kore strings for assembling the initial configuration +const PREFIX: &str = r#" +Lbl'-LT-'generatedTop'-GT-'{}( + Lbl'-LT-'T'-GT-'{}( + Lbl'-LT-'k'-GT-'{}( + kseq{}(inj{SortPgm{}, SortKItem{}}( + Lblinit'Unds'fuzz{}(\dv{SortInt{}}(""#; +const MIDFIX: &str = r#""),\dv{SortInt{}}(""#; +const POSTFIX: &str = r#""))), dotk{}())), Lbl'-LT-'state'-GT-'{}(Lbl'Stop'Map{}())), Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))"#; + +impl From for String { + /// Build the kore string to send off to kllvm's parser + fn from(input: FuzzInput) -> String { + let field1_str = input.field1.to_string(); + let field2_str = input.field2.to_string(); + + format!( + "{}{}{}{}{}", + PREFIX, field1_str, MIDFIX, field2_str, POSTFIX + ) + } +} + +fn main() { + kllvm::init(); + + // Free kllvm's memory when panicking. + panic::set_hook(Box::new(|_| { + kllvm::free_all_memory(); + })); + + loop { + fuzz!(|seed: &[u8]| { + let mut u = Unstructured::new(seed); + let Ok(input) = FuzzInput::arbitrary(&mut u) else { + panic!("Failed to generate input from seed"); + }; + + // Build the initial config, execute it, retrieve the final config kore string + let pattern_string: String = input.clone().into(); + let pattern: kllvm::Pattern = + pattern_string.parse().expect("Failed parsing kore string"); + let mut block: kllvm::Block = pattern.into(); + + block.take_steps(-1); + + let result: kllvm::Pattern = block.into(); + + // Parse the final kore string as [Pattern] for matching + let result_pattern: Pattern = Parser::new(&result.to_string()) + .unwrap() + .pattern() + .expect("Failed to parse result pattern"); + + match result_pattern { + Pattern::App(App { symbol, args, .. }, ..) => { + if symbol == SymbolId::new("Lbl'-LT-'generatedTop'-GT-'".to_string()).unwrap() { + let expected = args + .get(0) + .expect("Expected first argument of generatedTop to be present"); + match expected { + Pattern::App(App { symbol, .. }, ..) => { + if *symbol + == SymbolId::new("Lblfuzz'Unds'failure".to_string()).unwrap() + { + // FUZZ_FAILURE + panic!("Failure!"); + } + } + _ => panic!( + "Expected first argument of generatedTop to be an App pattern" + ), + } + } else { + panic!("Expected symbol for but found {:?}", symbol); + } + } + _ => panic!("Expected App pattern but found: {:?}", result_pattern), + }; + }); + } +} diff --git a/kframework_ffi/Cargo.lock b/kframework_ffi/Cargo.lock new file mode 100644 index 0000000..1d97779 --- /dev/null +++ b/kframework_ffi/Cargo.lock @@ -0,0 +1,7 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "kframework_ffi" +version = "0.1.0" diff --git a/kframework_ffi/Cargo.toml b/kframework_ffi/Cargo.toml new file mode 100644 index 0000000..5ca9e28 --- /dev/null +++ b/kframework_ffi/Cargo.toml @@ -0,0 +1,3 @@ +[package] +name = "kframework_ffi" +version = "0.1.0" diff --git a/kframework_ffi/src/kllvm.rs b/kframework_ffi/src/kllvm.rs new file mode 100644 index 0000000..9328678 --- /dev/null +++ b/kframework_ffi/src/kllvm.rs @@ -0,0 +1,44 @@ +//! # kllvm +//! +//! A safe interface for the K framework's llvm backend execution engine. +//! +//! This module declares foreign functions which are expected to be linked in +//! from an external interpreter library built by the kframework. +//! +//! ## Example +//! +//! ```no_run +//! use kframework_ffi::kllvm; +//! +//! const KORE_STRING: &str = "Lbl'-LT-'generatedTop'-GT-'{}( ..."; +//! +//! kllvm::init(); +//! +//! let pattern: kllvm::Pattern = KORE_STRING.parse().expect("Parsing failed!"); +//! let mut block: kllvm::Block = pattern.into(); +//! +//! block.take_steps(-1); +//! +//! let result: kllvm::Pattern = block.into(); +//! +//! println!("{result}"); +//! +//! kllvm::free_all_memory(); +//! ``` +mod block; +mod ffi; +mod pattern; + +pub fn init() { + unsafe { + ffi::kllvm_init(); + } +} +pub fn free_all_memory() { + unsafe { + ffi::kllvm_free_all_memory(); + } +} + +pub use self::block::Block; +pub use self::pattern::Pattern; diff --git a/kframework_ffi/src/kllvm/block.rs b/kframework_ffi/src/kllvm/block.rs new file mode 100644 index 0000000..e2f2a4b --- /dev/null +++ b/kframework_ffi/src/kllvm/block.rs @@ -0,0 +1,38 @@ +use super::ffi; +use super::Pattern; + +/// A safe wrapper around a foreign pointer to kllvm's interned representation. +/// kllvm's garbage collector manages the allocation/freeing of this pointer. +pub struct Block { + pub(crate) block: *const ffi::block, +} + +impl Block { + pub fn new(pattern: &Pattern) -> Self { + let result = unsafe { ffi::kore_pattern_construct(pattern.pattern) }; + Self { block: result } + } + + /// Execute the semantics for a given number of steps over the term. + /// + /// Pass `-1` to `steps` to execute until no more rules apply. + /// + /// Note that the current pointer will likely be cleaned up by kllvm's garbage + /// collection during execution and will no longer be a valid pointer, so + /// the Block will be updated to point at the resulting term. + pub fn take_steps(&mut self, steps: i64) { + self.block = unsafe { ffi::take_steps(steps, self.block) }; + } +} + +impl From for Block { + fn from(pattern: Pattern) -> Block { + Self::new(&pattern) + } +} + +impl From<&Pattern> for Block { + fn from(pattern: &Pattern) -> Block { + Self::new(pattern) + } +} diff --git a/kframework_ffi/src/kllvm/ffi.rs b/kframework_ffi/src/kllvm/ffi.rs new file mode 100644 index 0000000..9e997cc --- /dev/null +++ b/kframework_ffi/src/kllvm/ffi.rs @@ -0,0 +1,29 @@ +use std::ffi::{c_char, c_void}; + +#[repr(C)] +pub struct block { + _private: [u8; 0], // Unused field. Makes rust happy about FFI safety. +} + +#[repr(C)] +pub struct kore_pattern { + _private: [u8; 0], // Unused field. Makes rust happy about FFI safety. +} + +#[allow(dead_code)] +unsafe extern "C" { + /// Some strings from the llvm-backend are malloced, and we need to free them ourselves. + pub fn free(ptr: *const c_void) -> c_void; + + pub fn kllvm_init() -> c_void; + pub fn kllvm_free_all_memory() -> c_void; + + pub fn take_steps(steps: i64, subject: *const block) -> *const block; + + pub fn kore_pattern_parse(data: *const c_char) -> *const kore_pattern; + pub fn kore_pattern_dump(pattern: *const kore_pattern) -> *const c_char; + pub fn kore_pattern_free(pattern: *const kore_pattern) -> c_void; + + pub fn kore_pattern_construct(pattern: *const kore_pattern) -> *const block; + pub fn kore_pattern_from_block(subject: *const block) -> *const kore_pattern; +} diff --git a/kframework_ffi/src/kllvm/pattern.rs b/kframework_ffi/src/kllvm/pattern.rs new file mode 100644 index 0000000..2638e2b --- /dev/null +++ b/kframework_ffi/src/kllvm/pattern.rs @@ -0,0 +1,61 @@ +use super::ffi; +use super::Block; +use std::ffi::{c_void, CStr, CString}; +use std::fmt; +use std::str::FromStr; + +/// A safe wrapper around a pointer to kllvm's kore AST. +/// +/// kllvm expects the caller to free this object when it's +/// finished with it. `Drop` is implemented to do this. +pub struct Pattern { + pub(crate) pattern: *const ffi::kore_pattern, +} + +impl Pattern { + pub fn new(s: &str) -> Result::Err> { + Pattern::from_str(s) + } +} + +impl FromStr for Pattern { + type Err = String; + + fn from_str(s: &str) -> Result { + let c_str = match CString::new(s) { + Ok(s) => s.into_raw(), + Err(e) => return Err(format!("Error generating CString: {}", e)), + }; + let pattern = unsafe { ffi::kore_pattern_parse(c_str) }; + let _ = unsafe { CString::from_raw(c_str) }; // Free the CString memory + Ok(Self { pattern: pattern }) + } +} + +impl fmt::Display for Pattern { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + let result = unsafe { + let c_str = ffi::kore_pattern_dump(self.pattern); + let result = CStr::from_ptr(c_str) + .to_str() + .expect("Failed to convert kllvm::Pattern to &str") + .to_string(); + ffi::free(c_str as *const c_void); + result + }; + write!(f, "{}", result) + } +} + +impl From for Pattern { + fn from(subject: Block) -> Self { + let result = unsafe { ffi::kore_pattern_from_block(subject.block) }; + Self { pattern: result } + } +} + +impl Drop for Pattern { + fn drop(&mut self) { + unsafe { ffi::kore_pattern_free(self.pattern) }; + } +} diff --git a/kframework_ffi/src/lib.rs b/kframework_ffi/src/lib.rs new file mode 100644 index 0000000..8e0784e --- /dev/null +++ b/kframework_ffi/src/lib.rs @@ -0,0 +1,9 @@ +//! # kframework_ffi +//! +//! This crate provides the interface for foreign functions in the K framework. +//! +//! ## Notable Interfaces +//! +//! - [`kllvm::Pattern`]: kllvm's kore AST. +//! - [`kllvm::Block`]: kllvm's interned kore representation for execution. +pub mod kllvm;