From cd2435d0db541baf8b6b6605a4cf183e467e5849 Mon Sep 17 00:00:00 2001 From: Nick Spinale Date: Fri, 6 Oct 2023 08:19:28 +0000 Subject: [PATCH] Introduce the Kani Rust verifier - Add scripts in hacking/ - Add harness for sel4-bitfield-ops Signed-off-by: Nick Spinale --- crates/sel4/bitfield-ops/src/lib.rs | 89 +++++++++++++++++++++++++++-- hacking/kani/.gitignore | 1 + hacking/kani/Makefile | 14 +++++ hacking/kani/docker/Dockerfile | 34 +++++++++++ hacking/kani/docker/Makefile | 49 ++++++++++++++++ 5 files changed, 183 insertions(+), 4 deletions(-) create mode 100644 hacking/kani/.gitignore create mode 100644 hacking/kani/Makefile create mode 100644 hacking/kani/docker/Dockerfile create mode 100644 hacking/kani/docker/Makefile diff --git a/crates/sel4/bitfield-ops/src/lib.rs b/crates/sel4/bitfield-ops/src/lib.rs index 5d1647680..35ce0bcb8 100644 --- a/crates/sel4/bitfield-ops/src/lib.rs +++ b/crates/sel4/bitfield-ops/src/lib.rs @@ -15,12 +15,16 @@ pub trait UnsignedPrimInt: + BitOrAssign + Shl + Shr - + Default // HACK for generic 0 + + From // HACK for generic 0 and 1 { const NUM_BITS: usize = mem::size_of::() * 8; fn zero() -> Self { - Default::default() + false.into() + } + + fn one() -> Self { + true.into() } } @@ -109,6 +113,11 @@ impl UnsignedPrimIntExt for T {} // // // +pub fn get_bit(src: &[T], i: usize) -> bool { + assert!(i < src.len() * T::NUM_BITS); + src[i / T::NUM_BITS] & (T::one() << (i % T::NUM_BITS)) != T::zero() +} + pub fn get_bits>( src: &[T], src_range: Range, @@ -193,6 +202,18 @@ pub fn set_bits_from_slice( ) where T: TryFrom, usize: TryFrom, +{ + set_bits_from_slice_via::<_, _, usize>(dst, dst_range, src, src_start) +} + +fn set_bits_from_slice_via( + dst: &mut [T], + dst_range: Range, + src: &[U], + src_start: usize, +) where + T: TryFrom, + V: TryFrom, { let num_bits = dst_range.len(); @@ -202,11 +223,11 @@ pub fn set_bits_from_slice( let mut cur_xfer_start = 0; while cur_xfer_start < num_bits { - let cur_xfer_end = num_bits.min(cur_xfer_start + usize::NUM_BITS); + let cur_xfer_end = num_bits.min(cur_xfer_start + V::NUM_BITS); let cur_xfer_src_range = (src_start + cur_xfer_start)..(src_start + cur_xfer_end); let cur_xfer_dst_range = (dst_range.start + cur_xfer_start)..(dst_range.start + cur_xfer_end); - let xfer: usize = get_bits(src, cur_xfer_src_range); + let xfer: V = get_bits(src, cur_xfer_src_range); set_bits(dst, cur_xfer_dst_range, xfer); cur_xfer_start = cur_xfer_end; } @@ -377,3 +398,63 @@ mod test { } } } + +#[cfg(kani)] +mod verification { + use super::*; + + #[kani::proof] + #[kani::unwind(4)] + fn slice_ops() { + slice_ops_generic::(kani::any()); + slice_ops_generic::(kani::any()); + slice_ops_generic::(kani::any()); + slice_ops_generic::(kani::any()); + } + + // The type of kani::any() can't depend on generic parameters, so we pass the arrays as args. + fn slice_ops_generic((a, b): ([T; N], [U; M])) + where + T: UnsignedPrimInt + TryFrom, + U: UnsignedPrimInt + TryFrom, + V: UnsignedPrimInt + TryFrom + TryFrom, + { + let n: usize = kani::any(); + let start_a: usize = kani::any(); + let start_b: usize = kani::any(); + + kani::assume(n <= a.len()); + kani::assume(n <= b.len()); + kani::assume( + start_a + .checked_add(n) + .map(|end| end <= a.len()) + .unwrap_or(false), + ); + kani::assume( + start_b + .checked_add(n) + .map(|end| end <= b.len()) + .unwrap_or(false), + ); + + let range_a = start_a..(start_a + n); + + let mut a_mut = a; + + set_bits_from_slice_via::<_, _, V>(&mut a_mut, range_a.clone(), &b, start_b); + + let i: usize = kani::any(); + kani::assume(i < a.len() * T::NUM_BITS); + + let val = get_bit(&a_mut, i); + + let val_expected = if range_a.contains(&i) { + get_bit(&b, i - start_a + start_b) + } else { + get_bit(&a, i) + }; + + assert_eq!(val, val_expected); + } +} diff --git a/hacking/kani/.gitignore b/hacking/kani/.gitignore new file mode 100644 index 000000000..b83d22266 --- /dev/null +++ b/hacking/kani/.gitignore @@ -0,0 +1 @@ +/target/ diff --git a/hacking/kani/Makefile b/hacking/kani/Makefile new file mode 100644 index 000000000..6ba8eef92 --- /dev/null +++ b/hacking/kani/Makefile @@ -0,0 +1,14 @@ +BUILD ?= . + +build_dir := $(BUILD) +target_dir := $(build_dir)/target + +crates := \ + sel4-bitfield-ops + +.PHONY: none +none: + +.PHONY: check +check: + cargo kani --target-dir=$(abspath $(target_dir)) $(addprefix -p,$(crates)) diff --git a/hacking/kani/docker/Dockerfile b/hacking/kani/docker/Dockerfile new file mode 100644 index 000000000..52062f680 --- /dev/null +++ b/hacking/kani/docker/Dockerfile @@ -0,0 +1,34 @@ +FROM debian:bookworm + +RUN apt-get update -q && apt-get install -y --no-install-recommends \ + bash-completion \ + build-essential \ + ca-certificates \ + curl \ + make \ + man \ + procps \ + python3-pip \ + sudo \ + vim \ + && rm -rf /var/lib/apt/lists/* + +ARG UID +ARG GID + +RUN groupadd -f -g $GID x && useradd -u $UID -g $GID -G sudo -m -p x x +RUN echo '%sudo ALL=(ALL) NOPASSWD:ALL' >> /etc/sudoers # for convenience + +USER x + +# Optimize by matching rust-toolchain.toml +ENV DEFAULT_TOOLCHAIN=nightly-2023-08-02 + +RUN curl -sSf https://sh.rustup.rs | \ + bash -s -- -y --no-modify-path --default-toolchain $DEFAULT_TOOLCHAIN + +ENV PATH=/home/x/.cargo/bin:$PATH + +RUN cargo install --locked kani-verifier && cargo kani setup + +WORKDIR /work diff --git a/hacking/kani/docker/Makefile b/hacking/kani/docker/Makefile new file mode 100644 index 000000000..6bdd190cf --- /dev/null +++ b/hacking/kani/docker/Makefile @@ -0,0 +1,49 @@ +work_root := ../../.. +here_relative := hacking/kani + +id := rust-sel4-kani +image_tag := $(id) +container_name := $(id) + +uid := $(shell id -u) +gid := $(shell id -g) + +mount_params := type=bind,src=$(abspath $(work_root)),dst=/work + +.PHONY: none +none: + +.PHONY: build +build: + docker build \ + --build-arg UID=$(uid) --build-arg GID=$(gid) \ + -t $(image_tag) . + +.PHONY: run +run: build + docker run -d --name $(container_name) \ + --mount $(mount_params) \ + $(image_tag) sleep inf + +.PHONY: runi +runi: build + docker run --rm \ + --mount $(mount_params) \ + -it $(image_tag) bash + +.PHONY: exec +exec: + docker exec -it $(container_name) bash + +.PHONY: rm-container +rm-container: + for id in $$(docker ps -aq -f "name=^$(container_name)$$"); do \ + docker rm -f $$id; \ + done + +.PHONY: check +check: build + docker run --rm \ + --mount $(mount_params),readonly \ + -i $(image_tag) \ + make -C $(here_relative) check BUILD=/tmp/build