Rust-verification-tools - RVT is a collection of tools/libraries to support both static and dynamic verification of Rust programs.

Last update: Dec 31, 2022

Related tags

Security tools rust verification fuzzing klee seahorn proptest

Overview

Rust verification tools

This is a collection of tools/libraries to support both static and dynamic verification of Rust programs.

We see static verification (formal verification) and dynamic verification (testing) as two parts of the same activity and so these tools can be used for either form of verification.

Dynamic verification using the proptest fuzzing/property testing library.
Static verification using the KLEE symbolic execution engine.

We aim to add other backends in the near future.

In addition, we document how the tools we wrote work in case you are porting a verification tool for use with Rust. (In particular, we describe how to generate LLVM bitcode files that can be used with LLVM-based verification tools.)

Tools and libraries

verification-annotations crate: an FFI layer for creating symbolic values in KLEE
propverify crate: an implementation of the proptest library for use with static verification tools.
cargo-verify: a tool for compiling a crate and either verifying main/tests or for fuzzing main/tests. (Use the --backend flag to select which.)
compatibility-test test crate: test programs that can be verified either using the original proptest library or using propverify. Used to check that proptest and propverify are compatible with each other.

Usage

TL;DR

Install For installation with Docker, see the Usage section of our main docs.
Fuzz some examples with proptest
```
cd compatibility-test
cargo test
cd ..
```
(You can also use cargo-verify --backend=proptest --verbose.)

One test should fail – this is correct behaviour.
Verify some examples with propverify

cd verification-annotations; cargo-verify --tests

cd verification-annotations; cargo-verify --tests

No tests should fail.
Read the propverify intro for an example of fuzzing with proptest and verifying with propverify.
Read the proptest book
Read the source code for the compatibility test suite.

(Many of these examples are taken from or based on examples in the proptest book.)

There is also some limited documentation of how this works.

License

Licensed under either of

Apache License, Version 2.0 (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)

at your option.

Acknowledgements

The propverify crate is heavily based on the design and API of the wonderful proptest property/fuzz-testing library. The implementation also borrows techniques, tricks and code from the implementation – you can learn a lot about how to write an embedded DSL from reading the proptest code.

In turn, proptest was influenced by the Rust port of QuickCheck and the Hypothesis fuzzing/property testing library for Python. (proptest also acknowledges regex_generate – but we have not yet implemented regex strategies for this library.)

Known limitations

This is not an officially supported Google product; this is an early release of a research project to enable experiments, feedback and contributions. It is probably not useful to use on real projects at this stage and it may change significantly in the future.

Our current goal is to make propverify as compatible with proptest as possible but we are not there yet. The most obvious features that are not even implemented are support for using regular expressions for string strategies, the Arbitrary trait, proptest-derive.

We would like the propverify library and the cargo-verify script to work with as many Rust verification tools as possible and we welcome pull requests to add support. We expect that this will require design/interface changes.

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.

See the contribution instructions for further details.

Comments

Add Github actions-based workflow to build and push Docker images
Hello,

This is a proposal to have the Docker images built regularly (or on push to git branches following a specific pattern as needed) so that they can be pulled from a registry by anyone who would like to run the rust verification tools (provided they'd be better off downloading images from a registry instead of having to build them, which could be argued against as the resulting images are pretty heavy: ~1.7 GB after compression according to Docker registry).

More details about this pull-request can be found in this issue

Pre-merge requirements

[x] Remove user_uid, user_gid, username and ubuntu version params from matrix definition

[ ] Replacing the target docker image names in the GitHub action configuration file :

for rust base image

for all other images

[ ] Having the maintainers declared DOCKERHUB_USERNAME and DOCKERHUB_TOKEN values in the project settings Docker hub tokens can be generated from https://hub.docker.com/settings/security

cla: yes
opened by thierrymarianne 8
when use klee

Hello, I want to use klee to analyse some rust program and I set up my environment in a ubuntu18.04 docker following your docs. However, when I want to analyse the compiled file using klee --output-dir=kleeout --warnings-only-to-file target/debug/deps/try_klee*.bc, some error occured.The full error information is attached. I wonder how to fix it. Thanks a lot.
docker

opened by StevenJiang1110 7

docker/build script fails to build klee

Full output lives here: docker-build-output.txt and I have included a hopefully-relevant snippet below.

I don't have any experience with klee, so I haven't tried digging into this too deeply.

I did notice that we have UCLIBC_VERSION defined as klee_uclibc_v1.2 in docker/mkimage but it's not used anywhere. There are about 6 commits between https://github.com/klee/klee-uclibc.git HEAD and klee_uclibc_v1.2, so my current theory is that it might be one of those.

I had also removed the sudo around the docker calls, because my user already has permission to use docker (on macos). I'm currently doing a full-rebuild with sudo enabled and git checkout UCLIBC_VERSION in docker/klee/build_klee. I will tell you how it goes.

I do wonder whether it would be worthwhile publishing the relevant docker images somewhere. This would also help with https://github.com/project-oak/rust-verification-tools/issues/2 , and it's a workflow that people will be used to if they have used cross before.

 > [9/9] RUN sh build_klee:                                                                                                        
#14 0.331 Cloning into 'klee-uclibc'...                                                                                            
#14 4.260 INFO:Forcing C compiler to be.../usr/bin/clang-10
#14 4.260 INFO:Absolute path to compiler.../usr/bin/clang-10
#14 4.260 INFO:Disabling assertions
#14 4.260 INFO:Configuring for Debug build
#14 4.260 INFO:Configuring for LLVM bitcode archive
...
#14 161.5 [ 93%] Built target RuntimeFortify
#14 161.5 [ 93%] Built target BuildKLEERuntimes
#14 161.6 [ 94%] Built target kleeModule
#14 161.6 [ 97%] Built target kleeCore
#14 161.7 [ 97%] Built target klee
#14 161.7 Scanning dependencies of target systemtests
#14 161.7 [ 97%] Running system tests
#14 161.8 -- Testing: 346 tests, 4 workers --
#14 161.8 Testing:  0.. 10.. 20.. 30.. 40.. 50.. 60..
#14 185.0 FAIL: KLEE :: Runtime/POSIX/FD_Fail.c (241 of 346)
#14 185.0 ******************** TEST 'KLEE :: Runtime/POSIX/FD_Fail.c' FAILED ********************
#14 185.0 Script:
#14 185.0 --
#14 185.0 : 'RUN: at line 1';   /usr/bin/clang-10 -I/home/david/klee/include /home/david/klee/test/Runtime/POSIX/FD_Fail.c -emit-llvm -O0 -Xclang -disable-O0-optnone -c -o /home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp1.bc
#14 185.0 : 'RUN: at line 2';   rm -rf /home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out
#14 185.0 : 'RUN: at line 3';   /home/david/klee/build/bin/klee --output-dir=/home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out --libc=uclibc --posix-runtime /home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp1.bc --max-fail 1 | FileCheck /home/david/klee/test/Runtime/POSIX/FD_Fail.c
#14 185.0 --
#14 185.0 Exit Code: 2
#14 185.0 
#14 185.0 Command Output (stdout):
#14 185.0 --
#14 185.0 $ ":" "RUN: at line 1"
#14 185.0 $ "/usr/bin/clang-10" "-I/home/david/klee/include" "/home/david/klee/test/Runtime/POSIX/FD_Fail.c" "-emit-llvm" "-O0" "-Xclang" "-disable-O0-optnone" "-c" "-o" "/home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp1.bc"
#14 185.0 $ ":" "RUN: at line 2"
#14 185.0 $ "rm" "-rf" "/home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out"
#14 185.0 $ ":" "RUN: at line 3"
#14 185.0 $ "/home/david/klee/build/bin/klee" "--output-dir=/home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out" "--libc=uclibc" "--posix-runtime" "/home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp1.bc" "--max-fail" "1"
#14 185.0 # command stderr:
#14 185.0 KLEE: NOTE: Using POSIX model: /home/david/klee/build/runtime/lib/libkleeRuntimePOSIX64_Debug+Asserts.bca
#14 185.0 KLEE: NOTE: Using klee-uclibc : /home/david/klee/build/runtime/lib/klee-uclibc.bca
#14 185.0 KLEE: output directory is "/home/david/klee/build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out"
#14 185.0 KLEE: Using STP solver backend
#14 185.0 KLEE: WARNING: executable has module level assembly (ignoring)
#14 185.0 KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 94153668978176) at runtime/POSIX/fd.c:1007 10
#14 185.0 KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
#14 185.0 KLEE: WARNING ONCE: calling __klee_posix_wrapped_main with extra arguments.
#14 185.0 KLEE: ERROR: (location information missing) ASSERTION FAIL: f
#14 185.0 KLEE: NOTE: now ignoring this error at this location
#14 185.0 
#14 185.0 KLEE: done: total instructions = 30080
#14 185.0 KLEE: done: completed paths = 2
#14 185.0 KLEE: done: generated tests = 1
#14 185.0 
#14 185.0 $ "FileCheck" "/home/david/klee/test/Runtime/POSIX/FD_Fail.c"
#14 185.0 # command stderr:
#14 185.0 FileCheck error: '-' is empty.
#14 185.0 FileCheck command line:  FileCheck /home/david/klee/test/Runtime/POSIX/FD_Fail.c
#14 185.0 
#14 185.0 error: command failed with exit status: 2
#14 185.0 
#14 185.0 --
#14 185.0 
#14 185.0 ********************
#14 185.0 Testing:  0.. 10.. 20.. 30.. 40.. 50.. 60.. 70.. 80.. 90.. 
#14 222.8 ********************
#14 222.8 Failed Tests (1):
#14 222.8   KLEE :: Runtime/POSIX/FD_Fail.c
#14 222.8 
#14 222.8 
#14 222.8 Testing Time: 60.97s
#14 222.8   Unsupported      :  28
#14 222.8   Passed           : 315
#14 222.8   Expectedly Failed:   2
#14 222.8   Failed           :   1
#14 222.8 make[3]: *** [test/CMakeFiles/systemtests.dir/build.make:63: test/CMakeFiles/systemtests] Error 1
#14 222.8 make[2]: *** [CMakeFiles/Makefile2:1752: test/CMakeFiles/systemtests.dir/all] Error 2
#14 222.8 make[1]: *** [CMakeFiles/Makefile2:854: CMakeFiles/check.dir/rule] Error 2
#14 222.8 make: *** [Makefile:164: check] Error 2

opened by alsuren 6

`cargo-verify` tutorial: `rvt-klee.bc` not found in docker

I'm trying to work through the tutorial to use cargo verify here, with the Docker instructions. I'm able to use cargo test for proptest as expected, but the verify/KLEE backend fails.

I'm running Ubuntu 20.04, Docker version 20.10.7, build 20.10.7-0ubuntu1~20.04.1

Command:

cargo-verify --backend=klee --tests --verbose

Expected result:

Running 1 test(s)
test multiply ... ERROR

test result: ERROR. 0 passed; 1 failed
VERIFICATION_RESULT: ERROR

Actual result:

Checking verify
  Building verify for verification
STDERR:     Finished dev [unoptimized + debuginfo] target(s) in 0.01s
ERROR - FAILED: 'llvm-link-10' terminated with exit code 1.

End of trace with -vvvvvv:

INFO - Running 'llvm-link-10' in '.' with command:
llvm-link-10 -o /home/ubuntu/rust-verification-tools/verify/target/x86_64-unknown-linux-gnu/debug/deps/verify-238da9e126f6d636.link.bc /home/rust-verification-tools/runtime/rvt-klee.bc /home/rust-verification-tools/simd_emulation/simd_emulation.bc /home/ubuntu/rust-verification-tools/verify/target/x86_64-unknown-linux-gnu/debug/deps/verify-238da9e126f6d636.bc
STDERR: llvm-link-10: /home/rust-verification-tools/runtime/rvt-klee.bc: error: Could not open input file: No such file or directory
STDERR: llvm-link-10: error:  loading file '/home/rust-verification-tools/runtime/rvt-klee.bc'
ERROR - FAILED: 'llvm-link-10' terminated with exit code 1.

Full reproduction:

> cat Cargo.toml 
[package]
name = "verify"
version = "0.1.0"
authors = ["ubuntu"]
edition = "2018"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]

[target.'cfg(verify)'.dependencies]
propverify = { path="/home/rust-verification-tools/propverify" }

[target.'cfg(not(verify))'.dependencies]
proptest = { version = "*" }

[features]
verifier-klee = ["propverify/verifier-klee"]
verifier-crux = ["propverify/verifier-crux"]
verifier-seahorn = ["propverify/verifier-seahorn"]
> cat src/main.rs 
#[cfg(not(verify))]
use proptest::prelude::*;
#[cfg(verify)]
use propverify::prelude::*;

proptest! {
    #[test]
    fn multiply(a in 1..=1000u32, b in 1..=1000u32) {
        let r = a*b;
        prop_assert!(1 <= r && r < 1000000);
    }
}
> cargo test
   Compiling libc v0.2.102
   Compiling cfg-if v1.0.0
   Compiling ppv-lite86 v0.2.10
   Compiling autocfg v1.0.1
   Compiling remove_dir_all v0.5.3
   Compiling fnv v1.0.7
   Compiling bit-vec v0.6.3
   Compiling quick-error v1.2.3
   Compiling quick-error v2.0.1
   Compiling bitflags v1.3.2
   Compiling byteorder v1.4.3
   Compiling regex-syntax v0.6.25
   Compiling lazy_static v1.4.0
   Compiling bit-set v0.5.2
   Compiling num-traits v0.2.14
   Compiling getrandom v0.2.3
   Compiling wait-timeout v0.2.0
   Compiling rand_core v0.6.3
   Compiling rand_chacha v0.3.1
   Compiling rand_xorshift v0.3.0
   Compiling rand v0.8.4
   Compiling tempfile v3.2.0
   Compiling rusty-fork v0.3.0
   Compiling proptest v1.0.0
   Compiling verify v0.1.0 (/home/ubuntu/rust-verification-tools/verify)
    Finished test [unoptimized + debuginfo] target(s) in 10.61s
     Running target/debug/deps/verify-ac0d8570681ea509

running 1 test
test multiply ... ok

test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out

> cargo clean
> cargo-verify --backend=klee --tests --verbose
Checking verify
  Building verify for verification
STDERR:    Compiling verification-annotations v0.1.0 (/home/rust-verification-tools/verification-annotations)
STDERR:    Compiling propverify v0.1.0 (/home/rust-verification-tools/propverify)
STDERR:    Compiling verify v0.1.0 (/home/ubuntu/rust-verification-tools/verify)
STDERR:     Finished dev [unoptimized + debuginfo] target(s) in 8.07s
ERROR - FAILED: 'llvm-link-10' terminated with exit code 1.

Apologies if I set something up incorrectly, and thanks!

opened by avanhatt 5

add dockerfile and scripts to build image for rust-verification-tools(klee only)

These scripts and dockerfiles is to build rust-verification-tools(klee only) docker image. The building process almost follows the using-klee doc(three steps, install rust, install klee and install rust-verification-tools) but has some additional steps.(I think it may be essential) First, the script compiles cargo from source to work as the default cargo for the compiled rustc, so it leads to a stage2 compiling. Second, the script installs rustup from official scripts and choose stage2 as the default toolchain. The try-klee example has been added to the image for test use and it can work properly. However, when I try to follow the example replay input values in doc , there is still one link error. I have mentioned this in #36 .
cla: yes

opened by StevenJiang1110 5
Rust cargo verify

Rewrite of cargo-verify in rust. All the features were copied from the python script, but not very well tested. Some of the command line arguments were changed, see --help.
cla: yes

opened by fshaked 4
Support for symbolic strings
Composed of

Efficient support for creating symbolic Vec.

Tests involving strings

Creating a new top-level directory 'runtime' to contain C support code required to interface between what the Rust library expects from the C library and the set of operations provided by different verifiers.

This will probably end up being a combination of code that is needed by all verifiers and code that is only needed with a subset of the verifier backends that we support. So it will end up requiring conditional compilation.

For now all it contains is support for allocating aligned memory blocks (used by crates like Regex).

In the near future, I will add code to support code that uses pthreads but only requires one thread. (i.e., to support almost every thread-safe library)

Tests involving the standard Regex crate

cla: yes
opened by alastairreid 4

docker/build fails

I'm getting some errors running the build script; the 'klee' container fails, complaining about a missing header:

make[2]: *** [runtime/POSIX/fd_init32_Release+Debug+Asserts.bc] Error 1
In file included from /root/klee/klee/runtime/klee-libc/strncpy.c:37:                                                                                                                                             
/usr/include/stdlib.h:25:10: fatal error: 'bits/libc-header-start.h' file not found                                                                                                                               
#include <bits/libc-header-start.h>                                                                                                                                                                               
         ^~~~~~~~~~~~~~~~~~~~~~~~~~                                                                                                                                                                               
In file included from /root/klee/klee/runtime/klee-libc/putchar.c:10:                                                                                                                                             
/usr/include/stdio.h:27:10: fatal error: 'bits/libc-header-start.h' file not found                                                                                                                                
#include <bits/libc-header-start.h>                                                                                                                                                                               
         ^~~~~~~~~~~~~~~~~~~~~~~~~~                                                                                                                                                                               
In file included from /root/klee/klee/runtime/klee-libc/strcoll.c:10:                                                                                                                                             
/usr/include/string.h:26:10: fatal error: 'bits/libc-header-start.h' file not found                                                                                                                               
#include <bits/libc-header-start.h>                                                                                                                                                                               
         ^~~~~~~~~~~~~~~~~~~~~~~~~~                                                                                                                                                                               
In file included from /root/klee/klee/runtime/klee-libc/strtol.c:34:                                                                                                                                              
In file included from /usr/lib/llvm-10/lib/clang/10.0.0/include/limits.h:21:                                                                                                                                      
/usr/include/limits.h:26:10: fatal error: 'bits/libc-header-start.h' file not found                                                                                                                               
#include <bits/libc-header-start.h>                                                                                                                                                                               
         ^~~~~~~~~~~~~~~~~~~~~~~~~~                                                                                                                                                                               
1 error generated.                                                                                                                                                                                                
1 error generated.

It looks like the scripts are just pulling from the master branch directly; do you have a SHA that's verified to work for klee?

opened by mullr 4

fix broken links in README.md

I noticed a couple of broken links when browsing around your repo, so I ran it through a link-checker while I was waiting for docker/build to run.

$ npx markdown-link-check README.md 
npx: installed 65 in 4.194s

FILE: README.md
[✓] https://github.com/AltSysrq/proptest
[✓] http://klee.github.io/
[✖] docs/README.md
[✖] docs/install-rust.md
[✖] docs/install-klee.md
[✖] docs/using-propverify.md
[✓] https://altsysrq.github.io/proptest-book/intro.html
[✓] compatibility-test/src
[✖] docs/installation.md
[✓] LICENSE-APACHE
[✓] http://www.apache.org/licenses/LICENSE-2.0
[✓] LICENSE-MIT
[✓] http://opensource.org/licenses/MIT
[✓] https://github.com/burntsushi/quickcheck
[✓] https://hypothesis.works/
[✓] CONTRIBUTING.md

16 links checked.

After this patch, npx markdown-link-check README.md is clean.

If you would prefer for me to link to the rendered versions on https://project-oak.github.io then I can do.

cla: yes

opened by alsuren 3

Docker: build libstd/libcore without vectorization

This fixes linking errors we were getting due to compiling libstd/libcore with vectorization enabled and compiling code we are verifying with vectorization disabled.
cla: yes

opened by alastairreid 3
cargo-verify: tweak verbosity

This incomplete change causes commands to only print stdout/stderr if their level is below the current verbosity.

To finish this off, I (Alastair) plan to add -q/--quiet support as well.
cla: yes

opened by alastairreid 3
Archive Project?

I believe that this project has ended and thus the repo should be archived (which will make the repo read-only and put a notice at the top). Apologies if work is still ongoing.

opened by indolering 0

LLVM-11 support

The experimental support for LLVM-11 does not fully work.

Verifying a program (i.e., that defines 'main') seems to work (but has not been tested extensively)
Verifying a function annotated with #[test] does not work: KLEE crashes during its preprocessing phase.
Almost all of the regression tests rely on #[test] and do not work.

The error seen with #[test] is as follows. (This is obtained by using cargo verify -vvvvvv then cutting and pasting the command used to invoke KLEE.)

[Long list of errors that look like the next three lines]
Instruction does not dominate all uses!
  %.i3348 = phi i64 [ <badref>, <badref> ], [ %.i3682, %2236 ], [ %.i3344, %2227 ]
  %2378 = insertelement <4 x i64> %.upto24216, i64 %.i3348, i32 3

PHI nodes not grouped at top of basic block!
  %.i0345 = phi i64 [ <badref>, <badref> ], [ %.i0679, %2236 ], [ %.i0341, %2227 ]
label %2370
in function _ZN4test9run_tests17h3c40b1ee8455d4dbE

LLVM ERROR: Broken function found, compilation aborted!
/usr/lib/llvm-11/lib/libLLVM-11.so.1(_ZN4llvm3sys15PrintStackTraceERNS_11raw_ostreamE+0x1f)[0x7fae470b242f]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(_ZN4llvm3sys17RunSignalHandlersEv+0x22)[0x7fae470b0762]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(+0xaa6905)[0x7fae470b2905]
/lib/x86_64-linux-gnu/libc.so.6(+0x46210)[0x7fae4612d210]
/lib/x86_64-linux-gnu/libc.so.6(gsignal+0xcb)[0x7fae4612d18b]
/lib/x86_64-linux-gnu/libc.so.6(abort+0x12b)[0x7fae4610c859]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(+0x9f9c28)[0x7fae47005c28]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(+0x9f9a48)[0x7fae47005a48]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(+0xc2295f)[0x7fae4722e95f]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(_ZN4llvm13FPPassManager13runOnFunctionERNS_8FunctionE+0x3b9)[0x7fae471c1579]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(_ZN4llvm13FPPassManager11runOnModuleERNS_6ModuleE+0x33)[0x7fae471c6b23]
/usr/lib/llvm-11/lib/libLLVM-11.so.1(_ZN4llvm6legacy15PassManagerImpl3runERNS_6ModuleE+0x3e0)[0x7fae471c1b90]
klee(+0xa34bf)[0x564c44ede4bf]
klee(+0x49e4c)[0x564c44e84e4c]
klee(+0x2cc9c)[0x564c44e67c9c]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3)[0x7fae4610e0b3]
klee(+0x3c16e)[0x564c44e7716e]
Aborted

It is not obvious what is going wrong here.

LLVM

opened by alastairreid 3

AArch64 Docker build error
Docker version 20.10.6, build 370c289 macOS 11.4 aarch64 on commit e58c6a54f2.

=> ERROR importing cache manifest from rvt_base:latest

I had to delete this line from docker/mkimage:

--cache-from="${DOCKER_IMAGE_NAME}:${DOCKER_VERSION}" \

This cache doesn't exist on the first build?
opened by chadbrewbaker 4
Klee examples does not build
Hi!

Despite of patching like mentioned in https://github.com/project-oak/rust-verification-tools/issues/137 (i.e. paths in Cargo.toml files and +nightly for cargo calls) , still does not compile:

cd demos/simple/klee bash verify.sh

output:

Compiling verification-annotations v0.1.0 (/home/gww-parity/github/project-oak/rust-verification-tools/verification-annotations) error: /home/gww-parity/github/project-oak/rust-verification-tools/verification-annotations/src/verifier/klee.rs:91:14: in function _ZN24verification_annotations8verifier4klee82_$LT$impl$u20$verification_annotations..traits..VerifierNonDet$u20$for$u20$f32$GT$15verifier_nondet17h03b474201f344241E float (float): SSE register return with SSE disabled error: aborting due to previous error error: could not compile `verification-annotations` To learn more, run the command again with --verbose.

cargo +nightly build --features=verifier-klee --verbose Compiling verification-annotations v0.1.0 (/home/gww-parity/github/project-oak/rust-verification-tools/verification-annotations) Running rustc --crate-name verification_annotations --edition=2018 /home/gww-parity/github/project-oak/rust-verification-tools/verification-annotations/src/lib.rs --error-format=json --json=diagnostic-rendered-ansi --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --cfg 'feature="verifier-klee"' -C metadata=bbfe5df2a5b9d5c6 -C extra-filename=-bbfe5df2a5b9d5c6 --out-dir /home/gww-parity/github/project-oak/rust-verification-tools/demos/simple/klee/target/debug/deps -C incremental=/home/gww-parity/github/project-oak/rust-verification-tools/demos/simple/klee/target/debug/incremental -L dependency=/home/gww-parity/github/project-oak/rust-verification-tools/demos/simple/klee/target/debug/deps -Ctarget-feature=-mmx,-sse,-sse2,-sse3,-ssse3,-sse4.1,-sse4.2,-3dnow,-3dnowa,-avx,-avx2 -Cno-vectorize-loops -Cno-vectorize-slp -Copt-level=1 -Zpanic_abort_tests -Cpanic=abort -Warithmetic-overflow -Coverflow-checks=yes --cfg=verify -Clto -Cembed-bitcode=yes --emit=llvm-bc error: /home/gww-parity/github/project-oak/rust-verification-tools/verification-annotations/src/verifier/klee.rs:91:14: in function ZN24verification_annotations8verifier4klee82$LT$impl$u20$verification_annotations..traits..VerifierNonDet$u20$for$u20$f32$GT$15verifier_nondet17h03b474201f344241E float (float): SSE register return with SSE disabled

error: aborting due to previous error

error: could not compile verification-annotations

Caused by: process didn't exit successfully: rustc --crate-name verification_annotations --edition=2018 /home/gww-parity/github/project-oak/rust-verification-tools/verification-annotations/src/lib.rs --error-format=json --json=diagnostic-rendered-ansi --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --cfg 'feature="verifier-klee"' -C metadata=bbfe5df2a5b9d5c6 -C extra-filename=-bbfe5df2a5b9d5c6 --out-dir /home/gww-parity/github/project-oak/rust-verification-tools/demos/simple/klee/target/debug/deps -C incremental=/home/gww-parity/github/project-oak/rust-verification-tools/demos/simple/klee/target/debug/incremental -L dependency=/home/gww-parity/github/project-oak/rust-verification-tools/demos/simple/klee/target/debug/deps -Ctarget-feature=-mmx,-sse,-sse2,-sse3,-ssse3,-sse4.1,-sse4.2,-3dnow,-3dnowa,-avx,-avx2 -Cno-vectorize-loops -Cno-vectorize-slp -Copt-level=1 -Zpanic_abort_tests -Cpanic=abort -Warithmetic-overflow -Coverflow-checks=yes --cfg=verify -Clto -Cembed-bitcode=yes --emit=llvm-bc (exit status: 1)
opened by gww-parity 2

Use relative paths in demo/example Cargo.toml files

Example :

diff --git a/compatibility-test/Cargo.toml b/compatibility-test/Cargo.toml
index 7a18f73..2b31ff5 100644
--- a/compatibility-test/Cargo.toml
+++ b/compatibility-test/Cargo.toml
@@ -11,7 +11,7 @@ description = "Tests for both the propverify and the proptest crates - to check
 [dependencies]
 
 [target.'cfg(verify)'.dependencies]
-propverify = { path="/home/rust-verification-tools/propverify" }
+propverify = { path="../propverify" }
 
 [target.'cfg(not(verify))'.dependencies]
 proptest = { version = "*" }
diff --git a/demos/simple/klee/Cargo.toml b/demos/simple/klee/Cargo.toml
index 11fe766..fa1e6f4 100644
--- a/demos/simple/klee/Cargo.toml
+++ b/demos/simple/klee/Cargo.toml
@@ -5,7 +5,8 @@ authors = [""]
 edition = "2018"
 
 [dependencies]
-verification-annotations = { path="/home/rust-verification-tools/verification-annotations" }
+#verification-annotations = { path="/home/rust-verification-tools/verification-annotations" }
+verification-annotations = { path="../../../verification-annotations" }

btw. also maybe consider +nightly in scripts as it seems that some nightly features are required, example:

 cargo clean
-cargo build --features=verifier-klee
+cargo  +nightly build --features=verifier-klee

opened by gww-parity 4

Website link to RSS feed is broken

When I visit https://project-oak.github.io/rust-verification-tools/, there's a "subscribe via RSS" link that points to https://project-oak.github.io/rust-verification-tools/feed.xml (which according to View Source is actually a <link type="application/atom+xml", not RSS). However, RSS or Atom, this link is broken and points to a 404.

Is it possible to fix the link to enable subscribing in a RSS reader?

opened by nyanpasu64 1

Owner

GitHub https://project-oak.github.io/rust-verification-tools/

OpenSK is an open-source implementation for security keys written in Rust that supports both FIDO U2F and FIDO2 standards.

OpenSK This repository contains a Rust implementation of a FIDO2 authenticator. We developed OpenSK as a Tock OS application. We intend to bring a ful

2.4k Jan 7, 2023

Independent verification of binary packages - reproducible builds

rebuilderd(1) Independent verification system of binary packages. Accessing a rebuilderd instance in your browser Scripting access to a rebuilderd ins

311 Dec 30, 2022

Xori is an automation-ready disassembly and static analysis library for PE32, 32+ and shellcode

Xori - Custom disassembly framework Xori is an automation-ready disassembly and static analysis library that consumes shellcode or PE binaries and pro

712 Nov 28, 2022

Adds zero-cost stack overflow protection to your embedded programs

flip-link adds zero-cost stack overflow protection to your embedded programs The problem Bare metal Rust programs may not be memory safe in presence o

151 Dec 29, 2022

Whole program static stack analysis

cargo-call-stack Static, whole program stack analysis Other examples: Embedded CoAP / IPv4 server (source) "Hello, world!" HEADS UP: This tool relies

457 Dec 22, 2022

irulescan is a static security analyzer for iRules

irulescan is a tool to scan iRules for unexpected/unsafe expressions that may have undesirable effects like double substitution.

2 Dec 18, 2022

A library for building tools to determine if vulnerabilities are reachable in a code base.

Overview Vuln Reach is a library for developing tools that determine if a given vulnerability is reachable. Provided to the open source community by P

3 May 5, 2023

Kepler is a vulnerability database and lookup store and API currently utilising National Vulnerability Database and NPM Advisories as data sources

Kepler — Kepler is a vulnerability database and lookup store and API currently utilising National Vulnerability Database and NPM Advisories as data so

101 Nov 12, 2022

Steals browser passwords and cookies and sends to webhook.

Browser-Stealer Steals browser passwords and cookies and sends to webhook. Donating Educational Purposes Only This code is made so you can learn from

3 Sep 27, 2021

🕵️‍♀️ Find, locate, and query files for ops and security experts ⚡️⚡️⚡️

Recon Find, locate, and query files for ops and security experts Key Features • How To Use • Download • Contributing • License Key Features Query with

11 Dec 16, 2022

Detects usage of unsafe Rust in a Rust crate and its dependencies.

cargo-geiger ☢️ Looking for maintainer: https://github.com/rust-secure-code/cargo-geiger/issues/210 A program that lists statistics related to the usa

1.1k Jan 4, 2023

An esoteric language/compiler written with Rust and Rust LLVM bindings

MeidoLang (メイドラング) A not so useful and esoteric language. The goal of this project was to contain some quirky or novel syntax in a stack-style program

0 Dec 24, 2021

link is a command and control framework written in rust

link link is a command and control framework written in rust. Currently in alpha. Table of Contents Introduction Features Feedback Build Process Ackno

427 Dec 24, 2022

Rust library for building and running BPF/eBPF modules

RedBPF A Rust eBPF toolchain. Overview The redbpf project is a collection of tools and libraries to build eBPF programs using Rust. It includes: redbp

1.5k Jan 1, 2023

A rust program to bruteforce ZIP, PDF and some popular hashes.

Veldora A program to bruteforce zips, pdfs and some popular hashes. This is basically a rust version of bruttle, but a lot faster. Installation: git c

30 Dec 28, 2022

Advanced Fuzzing Library - Slot your Fuzzer together in Rust! Scales across cores and machines. For Windows, Android, MacOS, Linux, no_std, ...

LibAFL, the fuzzer library. Advanced Fuzzing Library - Slot your own fuzzers together and extend their features using Rust. LibAFL is written and main

1.2k Jan 6, 2023