Introduce the Kani Rust verifier

- Add scripts in hacking/ - Add harness for sel4-bitfield-ops Signed-off-by: Nick Spinale <[email protected]>
seL4 · Oct 7, 2023 · cd2435d · cd2435d
1 parent a2a147e
commit cd2435d
Show file tree

Hide file tree

Showing 5 changed files with 183 additions and 4 deletions.
diff --git 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<usize, Output = Self>
     + Shr<usize, Output = Self>
-    + Default // HACK for generic 0
+    + From<bool> // HACK for generic 0 and 1
 {
     const NUM_BITS: usize = mem::size_of::<Self>() * 8;
 
     fn zero() -> Self {
-        Default::default()
+        false.into()
+    }
+
+    fn one() -> Self {
+        true.into()
     }
 }
 
@@ -109,6 +113,11 @@ impl<T: UnsignedPrimInt> UnsignedPrimIntExt for T {}
 
 // // //
 
+pub fn get_bit<T: UnsignedPrimInt>(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<T: UnsignedPrimInt, U: UnsignedPrimInt + TryFrom<T>>(
     src: &[T],
     src_range: Range<usize>,
@@ -193,6 +202,18 @@ pub fn set_bits_from_slice<T: UnsignedPrimInt, U: UnsignedPrimInt>(
 ) where
     T: TryFrom<usize>,
     usize: TryFrom<U>,
+{
+    set_bits_from_slice_via::<_, _, usize>(dst, dst_range, src, src_start)
+}
+
+fn set_bits_from_slice_via<T: UnsignedPrimInt, U: UnsignedPrimInt, V: UnsignedPrimInt>(
+    dst: &mut [T],
+    dst_range: Range<usize>,
+    src: &[U],
+    src_start: usize,
+) where
+    T: TryFrom<V>,
+    V: TryFrom<U>,
 {
     let num_bits = dst_range.len();
 
@@ -202,11 +223,11 @@ pub fn set_bits_from_slice<T: UnsignedPrimInt, U: UnsignedPrimInt>(
 
     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::<u64, 3, u8, 3, u8>(kani::any());
+        slice_ops_generic::<u8, 3, u64, 3, u8>(kani::any());
+        slice_ops_generic::<u64, 3, u8, 3, u32>(kani::any());
+        slice_ops_generic::<u8, 3, u64, 3, u32>(kani::any());
+    }
+
+    // The type of kani::any() can't depend on generic parameters, so we pass the arrays as args.
+    fn slice_ops_generic<T, const N: usize, U, const M: usize, V>((a, b): ([T; N], [U; M]))
+    where
+        T: UnsignedPrimInt + TryFrom<V>,
+        U: UnsignedPrimInt + TryFrom<V>,
+        V: UnsignedPrimInt + TryFrom<T> + TryFrom<U>,
+    {
+        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
@@ -0,0 +1 @@
+/target/
diff --git a/hacking/kani/Makefile 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
@@ -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
@@ -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