search

model-checking / verify-rust-std

Verifying the Rust standard library
https://model-checking.github.io/verify-rust-std/
Other
161 stars 28 forks source link

Draft for tool proposal (goto-transcoder) #108

Open rafaelsamenezes opened 1 month ago

rafaelsamenezes commented 1 month ago

Dear team, We are opening this issue to obtain feedback on our initial proposal. The tool idea started as a discussion with @feliperodri at ETAPS and it would be great to see it moving forward.

Tool Name

Goto-transcoder (ESBMC)

Description

The goto-transcoder is an initiative to add a compatibility layer between GOTO programs generated from CPROVER tools (e.g., CBMC and goto-instrument). Specifically, we are interested in adding support to ESBMC. The main difference between ESBMC and CBMC is that ESBMC focuses on SMT and has support for other proof strategies such as incremental bounded model checking. For this proposal, we are concentrating in the conversion between CBMC goto -> ESBMC goto so that we can improve code reuse. Therefore, we can make use of Kani to generate a GOTO program for CBMC which can then be converted into an equivalent ESBMC input. 

flowchart LR
    R[Rust source] --> K[Kani]
    K -->|CBMC GBF| G[goto-transcoder]
    G -->|ESBMC GBF| ESBMC

ESBMC has a few differences to CBMC, including:

Tool Information

Yes, by converting the Kani goto program into an ESBMC-compatible one.

Yes. Similarly to CBMC, ESBMC's main use is for the verification of C programs, it has support for checking classical memory properties such as buffer overflow, dangling pointers, and memory leaks.

ESBMC is already integrated into the CI of industrial partners and it is also available in the GitHub actions marketplace for easy use. The transcoder is an independent Rust project that generates a binary that can be easily integrated into CI. We will need to work on the integration of Kani, goto-transcoder and ESBMC into a single CI job.

Both ESBMC and goto-transcoder have public development under permissive licenses, i.e., MIT and Apache 2.0.

ESBMC is a mature tool with active development, goto-transcoder is still in the initial phase (we have a list of what is currently supported).

Yes. ESBMC is a joint project of the Federal University of Amazonas (Brazil), the University of Manchester (UK), the University of Southampton (UK), and the University of Stellenbosch (South Africa).

The ESBMC development was supported by various research funding agencies, including CNPq (Brazil), CAPES (Brazil), FAPEAM (Brazil), EPSRC (UK), Royal Society (UK), British Council (UK), European Commission (Horizon 2020), and companies including ARM, Intel, Motorola Mobility, Nokia Institute of Technology and Samsung. The ESBMC development is currently funded by ARM, EPSRC grants EP/T026995/1 and EP/V000497/1, Ethereum Foundation, EU H2020 ELEGANT 957286, Intel, Motorola Mobility (through Agreement N° 4/2021), Soteria project awarded by the UK Research and Innovation for the Digital Security by Design (DSbD) Programme, and XC5 Hong Kong Limited.

Licenses

Steps to Use the Tool

For these steps let's verify a Rust hello world, we will assume that you have Kani available in your system. We will start with the Hello World from the Kani tutorial:

// File: test.rs
#[kani::proof]
fn main() {
    assert!(1 == 2);
}

Use Kani to generate the CBMC GOTO program

Invoke Kani and ask it to keep the intermediate files: kani test.rs --keep-temps. This generates a .out file that is in the GBF format. We can double-check this by invoking it with CBMC: cbmc *test4main.out --show-goto-functions:

[...]
main /* _RNvCshu9GRFEWjwO_4test4main */
        // 12 file test.rs line 3 column 10 function main
        DECL _RNvCshu9GRFEWjwO_4test4main::1::var_0 : struct tag-Unit
        // 13 file /Users/runner/work/kani/kani/library/std/src/lib.rs line 44 column 9 function main
        DECL _RNvCshu9GRFEWjwO_4test4main::1::var_1 : struct tag-Unit
        // 14 file /Users/runner/work/kani/kani/library/std/src/lib.rs line 44 column 22 function main
        DECL _RNvCshu9GRFEWjwO_4test4main::1::var_2 : c_bool[8]
[...]

Convert the CBMC goto into ESBMC goto

  1. Clone goto-transcoder: git clone https://github.com/rafaelsamenezes/goto-transcoder.git
  2. Convert to the ESBMC file: cargo run -- --mode 0 --input <kani-out>.out --output file-esbmc.goto
     Running `target/debug/gototranscoder --mode 0 --input main.goto --output file-esbmc.goto`
[2024-10-09T13:07:20Z INFO  gototranscoder] Converting CBMC input into ESBMC
[2024-10-09T13:07:20Z INFO  gototranscoder] Done

This will generate the file-esbmc.goto, which can be used as the ESBMC input.

Invoke ESBMC

  1. Download and install the latest version of ESBMC, at the time of this writing we used 7.7: https://github.com/esbmc/esbmc/releases/tag/v7.7
  2. Invoke ESBMC with the program: esbmc --binary file-esbmc.goto.
Solving with solver Z3 v4.13.0
Runtime decision procedure: 0.001s
Building error trace

[Counterexample]

State 1 file test.rs line 4 column 5 function main thread 0
----------------------------------------------------
Violated property:
  file test.rs line 4 column 5 function main
  KANI_CHECK_ID_test.cbacc14fa409fc10::test_0
  0

VERIFICATION FAILED

Artifacts

ESBMC originally came from the idea of using SMT to improve the performance of BMC tools. The original work was awarded at ASE'23 with the Most Influential Paper award.

Awards

Links

Documentation

Selected publications

Users

CI & Versioning

ESBMC and goto-transcoder are both developed at GitHub using Git.

For CI pipelines the tools can either be invoked directly or integrated into a custom action. ESBMC already has an action.

tautschnig commented 1 month ago

Could you please describe the user-visible differences of goto-transcoder+ESBMC (to Kani, as the presently only tool in CI) that you'd know or expect?

rafaelsamenezes commented 1 month ago

Could you please describe the user-visible differences of goto-transcoder+ESBMC (to Kani, as the presently only tool in CI) that you'd know or expect?

Could you clarify a bit? If I understood correctly you mean how a user will see the output of the tool:

  1. ESBMC has it own counterexample (as the screenshot above shows) which contains the program trace.
  2. We could also try to integrate goto-transcoder+ESBMC into Kani as a backend.
tautschnig commented 1 month ago

Could you clarify a bit? If I understood correctly you mean how a user will see the output of the tool:

My apologies for the unclear request. What I am seeking to understand is what advantages (and possibly also: disadvantages) we should expect when using ESBMC. Looking at the idea of integrating goto-transcoder+ESBMC with Kani (the Kani team would very much appreciate a pull request to that effect!), can you describe scenarios where ESBMC would be able to prove properties that Kani with CBMC as back-end currently cannot prove (one idea that comes to my mind is the upcoming support for quantifiers in Kani)? Are there perhaps also situations where ESBMC would not be able to prove a property? Would you expect performance differences?

rafaelsamenezes commented 1 month ago

Thanks for the clarification.

What I am seeking to understand is the advantages (and possibly also the disadvantages) we should expect when using ESBMC.

Can you describe scenarios where ESBMC would be able to prove properties that Kani with CBMC as a back-end currently cannot prove?

Regarding performance, quantifiers could indeed be translated directly into SMT formulas. As for concrete examples, I don't have any where k-induction + SMT outperforms BMC + SAT, considering we are still in the early stages. One way to explore this is to check specific benchmarks at SV-COMP: SV-COMP 2024 results and identify similar C constructs.

Comparing the benchmarks where ESBMC returned a correct verdict and CBMC failed to reach a verdict (ignoring wrong results):

Now considering the cases where both ESBMC and CBMC returned the correct verdict (2207 benchmarks) in reachability:

tautschnig commented 4 weeks ago

Thanks @rafaelsamenezes and apologies for the delayed response. Could you please go ahead and create a (draft?) PR that integrates goto-transcoder/ESBMC into CI of this repository? Perhaps start with just one of the harnesses.