model-checking / kani Goto Github PK

View Code? Open in Web Editor NEW

1.9K 22.0 77.0 30.23 MB

Kani Rust Verifier

Home Page: https://model-checking.github.io/kani

License: Apache License 2.0

Rust 93.96% Python 3.82% Shell 1.87% C 0.30% C++ 0.05%

rust model-checking verification

kani's Introduction

The Kani Rust Verifier is a bit-precise model checker for Rust.

Kani is particularly useful for verifying unsafe code blocks in Rust, where the "unsafe superpowers" are unchecked by the compiler.

Kani verifies:

Memory safety (e.g., null pointer dereferences)
User-specified assertions (i.e., assert!(...))
The absence of panics (e.g., unwrap() on None values)
The absence of some types of unexpected behavior (e.g., arithmetic overflows)

Installation

To install the latest version of Kani (Rust 1.58+; Linux or Mac), run:

cargo install --locked kani-verifier
cargo kani setup

See the installation guide for more details.

How to use Kani

Similar to testing, you write a harness, but with Kani you can check all possible values using kani::any():

use my_crate::{function_under_test, meets_specification, precondition};

#[kani::proof]
fn check_my_property() {
   // Create a nondeterministic input
   let input = kani::any();

   // Constrain it according to the function's precondition
   kani::assume(precondition(input));

   // Call the function under verification
   let output = function_under_test(input);

   // Check that it meets the specification
   assert!(meets_specification(input, output));
}

Kani will then try to prove that all valid inputs produce acceptable outputs, without panicking or executing unexpected behavior. Otherwise Kani will generate a trace that points to the failure. We recommend following the tutorial to learn more about how to use Kani.

GitHub Action

Use Kani in your CI with model-checking/kani-github-action@VERSION. See the GitHub Action section in the Kani book for details.

Security

See SECURITY for more information.

Contributing

If you are interested in contributing to Kani, please take a look at the developer documentation.

License

Kani

Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0).

See LICENSE-APACHE and LICENSE-MIT for details.

Rust

Kani contains code from the Rust project. Rust is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.

See the Rust repository for details.

kani's People

Contributors

Stargazers

Watchers

kani's Issues

Simplify code for count intrinsics in next CBMC version

There are a couple of PRs that will add support for count builtins in CBMC. This will allow the count intrinsics code in RMC to be simplified and its regression tests to be enabled.

Implement intrinsic `assert_uninit_valid`

RMC-rustc interface: Existing RMC interface to rustc

Inventory of how we're currently hooked in (what features we use)

CI for regression testing

GitHub actions for regression testing and PR blocking

2021 Week 15: rebase off upstream

intrinisic copy regression test should include an example with an overlapping region

This should apply to both the main test, and the volatile atomic test.

Initial soundness backlog document

Refactor: review `codegen_alloc_in_memory`

The intended semantics of the function codegen_alloc_in_memory are difficult to infer from the code and the documentation. The semantics of the Allocation type is hard to understand, so the codegen of the Allocation data is hard to trust. The definition of codegen_alloc_in_memory allows the function to be called with an Allocation and a String name, but the name may or may not be present in the symbol table. It is hard to understand why any invocation would call with the name already in the symbol table. Consider rewriting this function to do nothing but create a new symbol in the table with the bit pattern type and a bit pattern value. Consider another function that transmutes the value to the type of a symbol already in the symbol table.

Codegen issue: vtable struct with duplicate components

This test requires an additional check in struct_type() of cbmc/goto_program/typ.rs to ensure that the struct's components are unique. In this case, the vtable contains two foo fn pointers.

trait A {
    fn foo(&self) -> i32;
}

trait B {
    fn foo(&self) -> i32;
}

trait T : A + B {
}

struct S {
    x : i32,
    y : i32,
}

impl S {
    fn new(a:i32, b:i32) -> S {
        S {x:a, y:b}
    }
    fn new_box(a:i32, b:i32) -> Box<dyn T> { 
        Box::new(S::new(a,b))
    }
}


impl A for S {
    fn foo(&self) -> i32{
        self.x
    }
}

impl B for S {
    fn foo(&self) -> i32{
        self.y
    }
}

impl T for S {
}

fn main() {
    let t = S::new_box(1,2);
    let a = <dyn T as A>::foo(&*t);
    assert!(a == 1);
    let b = <dyn T as B>::foo(&*t);
    assert!(b == 2);
}

2021 week 16: rebase off upstream

Ensure we are using volatile correctly

According to @danielsn:

volatile has two meanings: one is just that we can't reorder or drop the access, which CBMC never does.
It might also mean that reads should return nondet, which we don't currently model.

The code for this would be in intrinsics.rs

RMC-rustc interface: Existing proof tool interfaces to rustc

Summarize API for

Cranelift (#55)
Prusti (#56)
Crux-mir (#53)

in collaboration with their authors.

Demangling of variable names

Can we track the name of variables so we get
main::square::vol instead of main::Shape[0]::vtable main$$Shape[0]$$vtable_impl_for_&main$$Rectangle[0]?

RMC-rustc interface: cranelift rustc interface

Regression suite: add per-test commandline options

RMC-rustc interface: prusti rustc interface

We need to redesign how we handle stubbing rust code

Vector sort not supported

Needed in firecracker/balloon-compact example

Ensure that every `codegen_unimplemented` feature has a matching run-make test

Codegen issue: box mut dyn trait unhandled codegen_pointer_cast

use std::io::{sink, Write};

fn main() {
    let mut log : Box<dyn Write + Send> = Box::new(sink());
    let dest : Box<dyn Write + Send> = Box::new(log.as_mut());
}

Fails with an unhandled pointer cast exception.

Maintain a map from functions to integers to generate fresh variables

Instead of taking a c in gen_function_local_variable, maintain a map from fname to int, and generate fresh variables that way. Actually: why is this index needed at all? It seems to be part of constructing a name, but unique names shouldn't rely on someone hand-picking the right index. Instead, a map of names should be kept, and the next available slot should be chosen.

Consider having our own CBMC mode instead of just using "C"

diffblue/cbmc#6219

Additional test cases for ProjectionElement::ConstantIndex

Have cases that test what happens if the length is not greater than the min length

Add support for inline ASM

Codegen issue: Cast to fat pointer

#![feature(layout_for_ptr)]                                                                        
use std::mem;                                                                                      
use std::sync::Arc;                                                                                
use std::sync::Mutex;                                                                              

pub trait Subscriber {                                                                             
    fn process(&mut self);                                                                         
    fn interest_list(&self);                                                                       
}                                                                                                  

struct DummySubscriber {                                                                           
}                                                                                                  

impl DummySubscriber {                                                                             
    fn new() -> Self {                                                                             
        DummySubscriber {}                                                                         
    }                                                                                              
}                                                                                                  

impl Subscriber for DummySubscriber {                                                              
    fn process(&mut self) {}                                                                       
    fn interest_list(&self) {}                                                                     
}                                                                                                  

fn main() {                                                                                        
    let v = unsafe { mem::size_of_val_raw(&5i32) };                                                
    assert!(v == 4);                                                                               

    let x : [u8;13] = [0; 13];                                                                     
    let y: &[u8] = &x;                                                                             
    let v = unsafe { mem::size_of_val_raw(y) };                                                    
    assert!(v == 13);                                                                              

    let s : Arc<Mutex<dyn Subscriber>> = Arc::new(Mutex::new(DummySubscriber::new()));             
}

Extend unstable atomic tests with generic types

Currently unstable atomic tests use only u8 values, but we should extend them to work with all integer values supported in Kani.

RMC-rustc interface: crux-mir rustc interface

Review documentation before flipping public

Develop a prototype implementation for source-based coverage report generation

Source-based coverage report generation is an experimental feature of the Rust compiler that we need to explore further. A prototype implementation will allow us to discover any limitations that may influence the way we plan to structure the RMC testing suite.

`codegen_unimplemented` should assume validity constraints for its nondet return value

Implement the generation of dashboards

Given a structure and confidence scores.

Coordinate with SMACK team on potential shared infrastructure

Cleanup: consistent names for typing contexts

Rename typing contexts to be consistent with:

mcx = MIR typing context
gcx = GOTO typing context

Reorganize the current test folder structure

Depends on source-based coverage reports. The reorganization will probably follow a chapter-like structure that follows the Rust reference.

Find a more elegant replacement for the `codegen_simple_intrinsic` macro

Relevant comment in intrinsics.rs

        // Codegens a simple intrinsic: ie. one which maps directly to a matching goto construct
        // We need to use this macro form because of a known limitation in rust
        // `codegen_simple_intrinsic!(self.get_sqrt(), Type::float())` gives the error message:
        //   error[E0499]: cannot borrow `*self` as mutable more than once at a time
        //    --> src/librustc_codegen_llvm/gotoc/intrinsic.rs:76:63
        //    |
        // 76 |                 codegen_simple_intrinsic!(self.get_sqrt(), Type::double())
        //    |                 ---- ------------------------                 ^^^^ second mutable borrow occurs here
        //    |                 |    |
        //    |                 |    first borrow later used by call
        //    |                 first mutable borrow occurs here

        //  To solve this, we need to store the `self.get_sqrt()` into a temporary variable.
        //  Using the macro form allows us to keep the call as a oneliner, while still making rust happy.

use std::path::Path;

fn main() {
    let path = Path::new("./foo/bar.txt");
}

Fails with a can't cast exception

const SIZE1: usize = 1;
const SIZE2: usize = 2;

pub static TABLE1: [(u64, u64); SIZE1] = [
    (0, 0),
];

pub static TABLE2: [(u64, u64); SIZE2] = [
    (0, 0),
    (0, 0),
];

fn main() {
    assert!(TABLE1[0].0 == 0);
}

Fails with:

thread 'rustc' panicked at 'assertion failed: `(left == right)`
  left: `256`,
 right: `128`', compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs:686