Rust mid-level IR Abstract Interpreter

Related tags

Security tools MIRAI
Overview

MIRAI codecov deps.rs

MIRAI is an abstract interpreter for the Rust compiler's mid-level intermediate representation (MIR). It is intended to become a widely used static analysis tool for Rust.

Who should use MIRAI

MIRAI can be used as a linter that finds panics that may be unintentional or are not the best way to terminate a program. This use case generally requires no annotations and is best realized by integrating MIRAI into a CI pipeline.

MIRAI can also be used to verify correctness properties. Such properties need to be encoded into annotations of the source program.

A related use is to better document an API via explicit precondition annotations and then use MIRAI to check that the annotations match the code.

Finally, MIRAI can be used to look for security bugs via taint analysis (information leaks, code injection bugs, etc.) and constant time analysis (information leaks via side channels). Unintentional (or ill-considered) panics can also become security problems (denial of service, undefined behavior).

How to use MIRAI

You'll need to install MIRAI as described here for MacOS and Windows and here for Linux.

To run MIRAI, use cargo with RUSTC_WRAPPER set to mirai. Use rustup override set nightly-YYYY-MM-DD to make Cargo use the same version of Rust as MIRAI. See the above installation instruction to determine which version to use. If you forget to do that or use the wrong version, you'll see an error message complaining about a dynamic load library not being found.

The easiest way to get started is to first build your project in the normal way (with one exception: set RUSTFLAGS="-Z always_encode_mir --cfg="mirai" to force the rust compiler to include MIR into its compiled output and enable any MIRAI annotations that are present in the source code). Refer to this link for details on compiling a cargo project. When there are no compile errors, no lint errors and no test failures, you can proceed to the next step and run MIRAI. For example:

touch src/lib.rs
RUSTC_WRAPPER=mirai cargo test --no-run

You could also just use cargo check if you do not have unit tests with good code coverage. The reason that cargo test is recommended is because unit tests are good entry points for the analysis. If you use cargo check, also do an initial check rather than build for the dependencies that you do not want to analyze with MIRAI.

The touch command (which needs to reference a real file in your project) forces Cargo to re-run rustc and to not assume that its cached error messages are still correct.

This will likely produce some warnings, which you can then fix by adding annotations declared in this crate. Keep running cargo as above until there are no more warnings.

At this stage your code will be better documented and more readable. Perhaps you'll also have found and fixed a few bugs.

You can use the environment variable MIRAI_FLAGS to get cargo to provide command line options to MIRAI. The value is a string which can contain any of the following flags:

  • --diag=default|verify|library|paranoid: configures level of diagnostics. With default MIRAI will not report errors which are potential 'false positives'. With verify it will point out functions that may contain such errors. With library it will require explicit preconditions. With paranoid it will flag any issue that may be an error.
  • --single_func <name>: the name of a specific function you want to analyze.
  • --body_analysis_timeout <seconds>: the maximum number of seconds to spend analyzing a function body.
  • --call_graph_config <path_to_config>: path to configuration file for call graph generator (see Call Graph Generator documentation). No call graph will be generated if this is not specified.
  • --: any arguments after this marker are passed on to rustc.

You can get some insight into the inner workings of MIRAI by setting the verbosity level of log output to one of warn, info, debug, or trace, via the environment variable MIRAI_LOG.

Using MIRAI together with the Rust design by contracts crate

Support for MIRAI is available in the design by contracts crate. See the shopping cart example for usage.

Developing MIRAI

See the developer guide for instructions on how to build, run and debug MIRAI.

Full documentation

Road map

  • Stabilize MIRAI and get rid of crashing bugs.
  • Summaries for intrinsics and standard library functions without MIR.

Join the MIRAI community

See the CONTRIBUTING file for how to help out.

License

MIRAI is MIT licensed, as found in the LICENSE file.

Comments
  • Validation fails on Ubuntu 20.04

    Validation fails on Ubuntu 20.04

    Issue

    Generally speaking, MIRAI cannot work well on Ubuntu 20.04. It cannot verify for some programs. So I tried to run validate.sh and it failed on the integration test. I was thinking it's because of my environment is not clean enough, so I also tried to use it in docker (ubuntu:latest) and it also failed.

    Steps to Reproduce

    1. Start a container of ubuntu:latest and run necessary components like pkg-config, z3, openssl and clang

    2. Insatll MIRAI following the steps documented in documentation/linux.md

    3. Run validate.sh

    Expected Behavior

    exit without error

    Actual Results

    error: test failed, to rerun pass '-p mirai --test integration_tests'
    
    Caused by:
      process didn't exit successfully: `/home/v_chenhongbo04/MIRAI/target/debug/deps/integration_tests-a0b61660615a641b` (signal: 11, SIGSEGV: invalid memory reference)
    

    Environment

    rustc 1.60.0-nightly (bfe156467 2022-01-22)

    opened by ya0guang 12
  • Adding set operations to TagPropagationSet

    Adding set operations to TagPropagationSet

    Description

    This adds two convenience functions for constructing taint propagation masks easier. E.g. adding and removing propagation types from existing masks

    Type of change

    • [ ] Bug fix (non-breaking change which fixes an issue)
    • [x] New feature (non-breaking change which adds functionality)
    • [ ] Breaking change (fix or feature that would cause existing functionality to not work as expected)
    • [x] API change with a documentation update
    • [ ] Additional test coverage
    • [ ] Code cleanup or just keeping up with the latest Rustc nightly

    How Has This Been Tested?

    I added two test cases, one for each function that verifies the basic functionality

    Checklist:

    • [x] Fork the repo and create your branch from main.
    • [x] If you've added code that should be tested, add tests.
    • [x] If you've changed APIs, update the documentation.
    • [x] Ensure the test suite passes.
    • [x] Make sure your code lints.
    • [x] If you haven't already, complete your CLA here: https://code.facebook.com/cla
    CLA Signed 
    opened by JustusAdam 9
  • Debug MIRAI in CLion

    Debug MIRAI in CLion

    Hi everyone! I've just heard about MIRAI. The project is very exciting and I hope it will eventually become a part of IntelliJ Rust and RLS code analysis! However, while reading the documentation I was surprised to see that CLion doesn't support debugging MIRAI ([1] and [2]).

    I've just tried it out and seems like it works fine: Screenshot 2019-03-30 at 12 21 02

    All I have to do is to provide the DYLD_LIBRARY_PATH as specified: Screenshot 2019-03-30 at 12 35 29

    Also [3],

    debugging support for Rust is pretty much non existent

    I'm sorry to hear that. I'm working on new lldb formatters for Rust; in CLion, they are enabled by default and configurable via Preferences | Build, Execution, Deployment | Debugger | Data Views | Rust. I hope debugging support gets better, though there is no Evaluate expression for Rust yet. So I really want to know if something related to debugging frontend doesn't work properly or if you have some ideas to improve it (at frontend level, like formatters, watches, remote debugging and so on). If so, you can open an issue here.

    question 
    opened by ortem 9
  • Encode tag checks as SMT queries

    Encode tag checks as SMT queries

    Description

    This commit implements Z3 encoding for tag checks. To ensure that the expression domain is precise enough to reduce tag checks to SMT queries, UnknownTagCheck expressions now record values instead of paths. On the Z3 side, I declare a top-level logical predicate has_tag in a way that has_tag(path, tag) encodes an uninterpreted Boolean-valued function call that checks whether path is attached with tag or not. When MIRAI generates a Z3 AST for UnknownTagCheck { operand, tag, .. }, it invokes the general_has_tag(operand, tag) routine, which recursively synthesizes a tag-check query from sub-expressions. This routine works similar to AbstractValue::get_tags.

    This commit also includes several tests that indicate bugs or loss of precision. One is that when we tag a function parameter that is a struct, we don't know paths rooted at it so we don't tag its fields. The other is that the current methodology for copy_or_move_elements and attach_tag_to_elements only tries to split a path after enumerating paths rooted at the target path, so updating if ... { local1 } else { local2 } would not update local1.field or local2.field.

    Type of change

    • [ ] Bug fix (non-breaking change which fixes an issue)
    • [x] New feature (non-breaking change which adds functionality)
    • [ ] Breaking change (fix or feature that would cause existing functionality to not work as expected)
    • [ ] API change with a documentation update
    • [ ] Additional test coverage
    • [ ] Code cleanup or just keeping up with the latest Rustc nightly

    How Has This Been Tested?

    ./validate.sh ran MIRAI over Libra

    CLA Signed 
    opened by stonebuddha 7
  • How does the static analyzer work?

    How does the static analyzer work?

    I couldn't find the instructions for enabling the static analyzer in the documentation. For example, I want the compiler to raise an error in the following example:

    #[pre(i < a.len())]
    #[post(*a[i] == v)]
    fn update(a: &mut [Box<i32>], i: usize, v: i32) {
        *a[i] = v + 1;
    }
    

    Is it possible?

    opened by mhoseinzadeh 7
  • [Building MIRAI]  wrapper.h:1:10: fatal error: 'z3.h' file not found

    [Building MIRAI] wrapper.h:1:10: fatal error: 'z3.h' file not found

    Issue

    Run cargo install --locked --path ./checker failed due to

    failed to run custom build command for `z3-sys v0.7.1`
    

    Caused by

    process didn't exit successfully: `<PATHTOMIRAI>/target/release/build/z3-sys-1ee5d02118b012a6/build-script-build` (exit status: 101)
      --- stdout
      cargo:rerun-if-changed=build.rs
      cargo:rerun-if-changed=wrapper.h
    
      --- stderr
      wrapper.h:1:10: fatal error: 'z3.h' file not found
      wrapper.h:1:10: fatal error: 'z3.h' file not found, err: true
      thread 'main' panicked at 'Unable to generate bindings: ()', ~/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/build.rs:33:14
      note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
    error: failed to compile `mirai v1.1.0 (<PATHTOMIRAI>/checker)`, intermediate artifacts can be found at `<PATHTOMIRAI>/target`
    

    Steps to Reproduce

    1. brew info z3
    z3: stable 4.8.17 (bottled), HEAD
    High-performance theorem prover
    https://github.com/Z3Prover/z3
    /usr/local/Cellar/z3/4.8.17 (135 files, 94.9MB) *
      Poured from bottle on 2022-06-17 at 00:26:16
    
    1. git clone https://github.com/facebookexperimental/MIRAI.git
    2. cd MIRAI
    3. ./setup.sh
    4. cp binaries/libz3.dylib /usr/local/lib
    cp: /usr/local/lib/libz3.dylib: Permission denied
    

    manually copy succeeded, replaced the original libz3.dylib in /usr/local/lib 6. cargo install --locked --path ./checker

    Expected Behavior

    Successful build of MIRAI

    Actual Results

    Panic

    Environment

    macOS Monterey v12.3.1, Intel processor. Rust version: rustc 1.63.0-nightly (4c5f6e627 2022-05-17)

    opened by yanliu18 6
  • "Sorts (_ BitVec 128) and Int are incompatible"

    I tried to run MIRAI on one of our crate, but I got this error message:

    Error: Sorts (_ BitVec 128) and Int are incompatible
    error: could not compile `chain-core`.
    
    To learn more, run the command again with --verbose.
    

    I follow the doc to install recent MIRAI, runs something like this:

    $ export RUSTFLAGS="-Z always_encode_mir"
    $ cargo build -p chain-core
    $ touch $CRATE/src/lib.rs
    $ RUSTC_WRAPPER=mirai cargo build -p chain-core
    
    opened by yihuang 6
  • Lack of support for bitwise negation

    Lack of support for bitwise negation

    Issue

    MIRAI seems to treat all expressions like !e as logical negation, while Rust does support bitwise negation operation. This makes Z3 crash due to typing errors.

    Steps to Reproduce

    Run MIRAI for the utf8-range crate (v1.0.3) reproduces the crash. More specifically, the crash is triggered when analyzing the function Utf8Sequences::next.

    Expected Behavior

    The analysis should terminate without errors.

    Actual Results

    An error message from Z3 before crash: Error: Sort mismatch at argument #1 for function (declare-fun not (Bool) Bool) supplied sort is Int

    Environment

    Rust version 1.37.0-nightly (5f3656ce9 2019-06-11)

    opened by uraj 6
  • Add support for Windows installation

    Add support for Windows installation

    Description

    Added z3.lib to the binaries directory for Windows installation and added a build.rs file to allow Rust to locate the lib on Windows. Updated InstallationGuide.md to reflect this. Added Windows to .travis.yml build matrix.

    (Also changed "OSX" to "macOS" in InstallationGuide.md to reflect official renaming).

    Fixes: N/A

    Type of change

    • [ ] Bug fix (non-breaking change which fixes an issue)
    • [x] New feature (non-breaking change which adds functionality)
    • [ ] Breaking change (fix or feature that would cause existing functionality to not work as expected)
    • [ ] API change with a documentation update
    • [ ] Additional test coverage

    How Has This Been Tested?

    Installation with the change has been tested locally on both a Windows and on a macOS machine.

    Checklist:

    • [x] Fork the repo and create your branch from master.
    • [ ] If you've added code that should be tested, add tests.
    • [ ] If you've changed APIs, update the documentation.
    • [x] Ensure the test suite passes.
    • [x] Make sure your code lints.
    • [x] If you haven't already, complete your CLA here: https://code.facebook.com/cla
    CLA Signed 
    opened by darioncassel 6
  • [Discussion] Abstract heap

    [Discussion] Abstract heap

    I think we need an abstract model of heap. What is on your mind? @hermanventer

    Another question to clarify is how to abstract heap pointer values, a.k.a. Box<T>. Is there another wrapper of heap-allocated object in Rust?

    I checked the source and there is only pub environment: &'a mut HashTrieMap<Path, AbstractValue>.

    question 
    opened by izgzhen 6
  • How to verify tag when type changes

    How to verify tag when type changes

    Issue

    I want to verify a typestate program but I'm hindered by some unexpected output. So I start with a minimal reproducible example.

    When I have two structs (say A and B for example) and have a function converting from A to B. How should I maintain and propagate the tag? I checked annotations/lib.rs and found SubComponent and SuperComponent, but the output is not as what I expected. In the example below I verified the tag after executing a_to_b and has the same postcondition in a_to_b, however only the postcondition is not always satisfied.

    Steps to Reproduce

    // main.rs
    #![cfg_attr(mirai, allow(incomplete_features), feature(generic_const_exprs))]
    
    extern crate mirai_annotations;
    
    use mirai_annotations::*;
    
    #[cfg(mirai)]
    use mirai_annotations::TagPropagationSet;
    
    #[cfg(mirai)]
    struct SecretTaintKind<const MASK: TagPropagationSet> {}
    
    #[cfg(mirai)]
    const SECRET_TAINT: TagPropagationSet = TAG_PROPAGATION_ALL;
    
    #[cfg(mirai)]
    type SecretTaint = SecretTaintKind<SECRET_TAINT>;
    
    #[cfg(not(mirai))]
    type SecretTaint = ();
    
    struct A(u32);
    struct B(u32);
    
    fn a_to_b(a: A) -> B {
        precondition!(has_tag!(&a, SecretTaint));
        let b = B(a.0 + 1);
        postcondition!(has_tag!(&b, SecretTaint));
        b
    }
    
    fn main() {
        let a = A(1);
        add_tag!(&a, SecretTaint);
        let b = a_to_b(a);
        verify!(has_tag!(&b, SecretTaint));
    }
    

    run cargo mirai.

    Expected Behavior

    no warning.

    Actual Results

     test-mirai git:(master) ✗ cargo mirai
        Checking test-mirai v0.1.0 (/Users/ya0guang/test-mirai)
    [2022-02-02T02:16:39Z INFO  mirai] MIRAI options from environment: Options { single_func: None, test_only: false, diag_level: Default, constant_time_tag_name: None, max_analysis_time_for_body: 30, max_analysis_time_for_crate: 240, statistics: false, call_graph_config: None }
    [2022-02-02T02:16:39Z INFO  mirai] MIRAI options modified by command line: Options { single_func: None, test_only: false, diag_level: Default, constant_time_tag_name: None, max_analysis_time_for_body: 30, max_analysis_time_for_crate: 240, statistics: false, call_graph_config: None }
    [2022-02-02T02:16:39Z INFO  mirai::callbacks] Processing input file: src/main.rs
    [2022-02-02T02:16:39Z INFO  mirai::callbacks] storing summaries for src/main.rs at /var/folders/cv/mtjnjfxs14lbt801r9vm8sd40000gp/T/.tmpAuiOal/.summary_store.sled
    [2022-02-02T02:16:39Z INFO  mirai::summaries] creating a new summary store from the embedded tar file
    [2022-02-02T02:16:39Z INFO  mirai::crate_visitor] analyzing function test_mirai.main
    warning: possible unsatisfied postcondition
      --> src/main.rs:28:5
       |
    28 |     postcondition!(has_tag!(&b, SecretTaint));
       |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    
    warning: `test-mirai` (bin "test-mirai") generated 1 warning
        Finished dev [unoptimized + debuginfo] target(s) in 0.68s
    

    Besides, from the comments in annotations/lib.rs, I think postcondition! is flow-sensitive, but verify! is not when using them in the same place in the function.

    Environment

    rustc 1.60.0-nightly (bfe156467 2022-01-22)

    opened by ya0guang 5
  • Problems in tag analysis for vector operations

    Problems in tag analysis for vector operations

    Issue

    1. Adding tag to a vector doesn't propagate the tag to the elements in this vector.
    2. Unexpected tag analysis result when using into_iter() to iterate a vector of struct.

    Steps to Reproduce

    For problem 1, I found this test which exactly meets my verification conditions. MIRAI should not complain about this but it actually complains. However, this line is commented and I don't know why. I'd be more than grateful if you can provide more details.

    For the second problem, I create a vector of struct I and tag each element. When iterating the vector using into_iter, MIRAI can detect that elements have tags (provably false verification condition in the following snippet). However, when the lines are uncommented, MIRAI doesn't complain anymore, and I think this is problematic.

    #![cfg_attr(mirai, allow(incomplete_features), feature(generic_const_exprs))]
    extern crate mirai_annotations;
    use mirai_annotations::*;
    
    #[cfg(mirai)]
    use mirai_annotations::TagPropagationSet;
    #[cfg(mirai)]
    pub struct SecretTaintKind<const MASK: TagPropagationSet> {}
    #[cfg(mirai)]
    const SECRET_TAINT: TagPropagationSet = TAG_PROPAGATION_ALL;
    #[cfg(mirai)]
    pub type SecretTaint = SecretTaintKind<SECRET_TAINT>;
    
    use std::vec::Vec;
    
    struct I(u32);
    
    fn main() {
        let va = vec![I(1), I(2), I(3)];
    
        for i in va.iter() {
            add_tag!(i, SecretTaint);
        }
        let mut vb: Vec<I> = Vec::new();
        // let mut vb: Vec<i32> = Vec::new();
    
        for i in va.into_iter() {
            verify!(does_not_have_tag!(&i, SecretTaint));
            // vb.push(i);
        }
    }
    

    Expected Behavior

    When the commented lines are uncommented, MIRAI should complain at verify!(does_not_have_tag!(&i, SecretTaint));.

    Actual Results

    When the commented lines are uncommented, MIRAI doesn't complain.

    Environment

    rustc 1.61.0-nightly (c84f39e6c 2022-03-20)

    opened by ya0guang 0
  • Verify tag propagation for multiple type changes

    Verify tag propagation for multiple type changes

    Issue

    MIRAI cannot produce correct result in tag propagation when types are changing multiple times. In my previous issue #1131 , the problem is solved when there is one type change. However, when there are more than one type changes, MIRAI doesn't work.

    Steps to Reproduce

    #![cfg_attr(mirai, allow(incomplete_features), feature(generic_const_exprs))]
    extern crate mirai_annotations;
    use mirai_annotations::*;
    
    #[cfg(mirai)]
    use mirai_annotations::TagPropagationSet;
    #[cfg(mirai)]
    struct SecretTaintKind<const MASK: TagPropagationSet> {}
    #[cfg(mirai)]
    const SECRET_TAINT: TagPropagationSet = TAG_PROPAGATION_ALL;
    #[cfg(mirai)]
    type SecretTaint = SecretTaintKind<SECRET_TAINT>;
    #[cfg(not(mirai))]
    type SecretTaint = ();
    
    struct A(u32);
    struct B(u32);
    struct C(u32);
    
    fn a_to_b(a: A) -> B {
        precondition!(has_tag!(&a, SecretTaint));
        let b = B(a.0 + 1);
        b
    }
    
    fn b_to_c(b: B) -> C {
        precondition!(has_tag!(&b, SecretTaint));
        let c = C(b.0 + 1);
        c
    }
    
    fn main() {
        let a = A(1);
        add_tag!(&a, SecretTaint);
        let b = a_to_b(a);
        verify!(has_tag!(&b, SecretTaint));
        let c = b_to_c(b);
        verify!(has_tag!(&c, SecretTaint));
        println!("reachable?");
    }
    

    Expected Behavior

    Satisfied verification

    Actual Results

    MIRAI complains:

    $ cargo mirai
        Checking mirai_test v0.1.0 (/Users/v_chenhongbo04/Code/mirai_test)
    warning: unsatisfied precondition
      --> src/main.rs:43:13
       |
    43 |     let c = b_to_c(b);
       |             ^^^^^^^^^
       |
    note: related location
      --> src/main.rs:33:5
       |
    33 |     precondition!(has_tag!(&b, SecretTaint));
       |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
       = note: this warning originates in the macro `precondition` (in Nightly builds, run with -Z macro-backtrace for more info)
    
    warning: this is unreachable, mark it as such by using the verify_unreachable! macro
      --> src/main.rs:44:5
       |
    44 |     verify!(has_tag!(&c, SecretTaint));
       |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    
    warning: `mirai_test` (bin "mirai_test") generated 2 warnings
        Finished dev [unoptimized + debuginfo] target(s) in 0.72s
    

    Environment

    rustc 1.61.0-nightly (c84f39e6c 2022-03-20)

    I'm using the latest MIRAI with the same rust toolchain version.

    opened by ya0guang 0
  • Make k-limits into command line options

    Make k-limits into command line options

    Issue

    Currently a set of constants in checker/src/k_limits.rs provides limits on how much computation MIRAI will do in various places. With these limits in place, largish crates can be analyzed in a somewhat reasonable time frame. The limits do, however, impact on precision and may lead to false negatives. By making these into variables that can be set via command line options, it will become possible to schedule longer runs that may find more issues than more limited runs. The greater precision allowed by such runs can also be used to weed out false positives.

    The recommended way to complete this task is to turn the constants in k_limits into the fields of a struct and to provide a constructor that sets the fields to default values, along with a command line processor that updates the values from options in the command line.

    The limits struct should then be made part of the visitor state (checker/src/visitor.rs).

    Ideally, there should also be a way to set these options to non default values for integration test cases. See also #52.

    enhancement good first issue 
    opened by hermanventer 2
  • Meta Meta Issue: Create meta issues

    Meta Meta Issue: Create meta issues

    Issue

    We need more issues. Create some meta issues to spur the creation of more issues.

    Steps to Reproduce

    Look at the issues tab.

    Expected Behavior

    There should be more issues and meta issues.

    Actual Results

    Not enough issues.

    opened by hermanventer 0
  • Meta Issue: Code Coverage

    Meta Issue: Code Coverage

    Issue

    Some parts of the MIRAI code base are not covered by integration tests. You task here is to find such bits of code and to create an issue for each of them. Ideally follow up with a PR that contains a test case that covers that bit of code.

    Steps to Reproduce

    As you read through the code base to get to know it, click on the coverage button so see code coverage. The code coverage tools is not quite perfect, so you might see lines that are marked as not covered when they obviously are, but there will be some cases that are not obviously covered. You can verify that a line of code is not covered by setting a break point on it and running the integration tests from the debugger.

    If you are going to follow up with a PR to fix this omission, the next step would be to set some breakpoints in the surrounding covered code to find the test cases that reach then and then try to mutate one or more of those test cases to instead or also reach the uncovered code.

    Expected Behavior

    Every executable source line should be reached by an integration test case.

    Actual Results

    Some code lines are not so covered.

    good first issue 
    opened by hermanventer 0
  • Meta Issue: Fix developer instructions

    Meta Issue: Fix developer instructions

    Issue

    If you like compilers and related tools, you are a meta-programmer, so you should like meta issues as well. This issue is a task to create tasks.

    Since you are new here, please keep track of all of the surprises you've encountered and the things you had to find out the hard way. Then make an issue to get the fixed.

    Ideally, follow that up with PR in which you fix it. Many thanks for doing that!

    Steps to Reproduce

    Read the developer documentation and try to fix an issue.

    Expected Behavior

    You got going with no problems and everything is crystal clear.

    Actual Results

    You muttered WTF on several occasions.

    good first issue 
    opened by hermanventer 0
Releases(v1.1.3)
  • v1.1.3(Nov 29, 2022)

  • v1.1.2(Sep 29, 2022)

  • v1.1.0(Dec 21, 2021)

  • libra_v1.0.4(Sep 19, 2019)

    Use separate lock file to avoid panic in Sled. Only share the persistent store between crates if flag is present. Contracts for variants of rand.Rng.gen_range and rand.Rng.gen_bool. Give diagnostics if non public function is a call tree root. MIR assertions now treated just like verify.

    Source code(tar.gz)
    Source code(zip)
  • v1.0.3(Sep 11, 2019)

    Make --sysroot available for the command line. Add a rust-toolchain Make core::slice::Iter methods generic. Add def ids for un-summarized functions in the call graph being analyzed. Add (assume|verify)_unreachable macros. Make the result of an uninterpreted call more complete to allow better refinement. Promote pre/post conditions for async functions.

    Source code(tar.gz)
    Source code(zip)
  • libra_v1.0.3(Sep 11, 2019)

    Make --sysroot available for the command line. Add a rust-toolchain Make core::slice::Iter methods generic. Add def ids for un-summarized functions in the call graph being analyzed. Add (assume|verify)_unreachable macros. Make the result of an uninterpreted call more complete to allow better refinement. Promote pre/post conditions for async functions.

    Source code(tar.gz)
    Source code(zip)
  • v1.0.2(Aug 27, 2019)

    Standard library summaries for cmp::max. Use joins for conditional expressions with conditions that are TOP. Fix bug in refinement of conditional expressions. Apply binary operation distribution recursively during expression simplification. Discard join condition when joining backward branches (keeps path conditions simpler during fixed point loops).

    Source code(tar.gz)
    Source code(zip)
  • v1.0.1(Aug 16, 2019)

    Fixes a bug with name mangling when macros are involved. More standard library contracts. Updates dependencies. Ignores predecessor blocks that are known not to reach a block after round 1 of the fixed point loop. Fixes diagnostic formatting that resulted in "possible possible ..." messages.

    Source code(tar.gz)
    Source code(zip)
  • v1.0.0(Aug 2, 2019)

Owner
Meta Experimental
These are Meta projects that are not necessarily used in production but are being developed in the open nevertheless.
Meta Experimental
A high level language for SELinux policy

Introduction Cascade is a project to build a new high level language for defining SELinux policy. The overall structure of the language is essentially

Daniel Burgener 42 Dec 14, 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

Rust Secure Code Working Group 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

null 0 Dec 24, 2021
Rust-verification-tools - RVT is a collection of tools/libraries to support both static and dynamic verification of Rust programs.

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

null 253 Dec 31, 2022
Rust bindings for libinjection

libinjection-rs Rust bindings for libinjection. How to use Add libinjection to dependencies of Cargo.toml: libinjection = "0.2" Import crate: extern c

ArvanCloud 35 Sep 24, 2022
A simple password manager written in Rust

ripasso A simple password manager written in Rust. The root crate ripasso is a library for accessing and decrypting passwords stored in pass format (G

Joakim Lundborg 548 Dec 26, 2022
tcp connection hijacker, rust rewrite of shijack

rshijack tcp connection hijacker, rust rewrite of shijack from 2001. This was written for TAMUctf 2018, brick house 100. The target was a telnet serve

null 377 Jan 1, 2023
A fast, simple, recursive content discovery tool written in Rust.

A simple, fast, recursive content discovery tool written in Rust ?? Releases ✨ Example Usage ✨ Contributing ✨ Documentation ?? ?? What the heck is a f

epi 3.6k Dec 30, 2022
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

null 427 Dec 24, 2022
CVEs for the Rust standard library

Rust CVE Preface This is a list of CVEs for unsound APIs in the Rust standard library. These bugs break Rust's memory safety guarantee and lead to sec

Yechan Bae 26 Dec 4, 2022
Rust bindings for VirusTotal/Yara

yara-rust Bindings for the Yara library from VirusTotal. More documentation can be found on the Yara's documentation. Example The implementation is in

null 43 Dec 17, 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

foniod 1.5k Jan 1, 2023
Rust library for developing safe canisters.

IC Kit This library provides an alternative to ic-cdk that can help developers write canisters and unit test them in their Rust code. Install Add this

Psychedelic 26 Nov 28, 2022
MimiRust - Hacking the Windows operating system to hand us the keys to the kingdom with Rust.

MimiRust - Hacking the Windows operating system to hand us the keys to the kingdom with Rust. MimiRust is a program based on the wdigest attack vector

Thotty 0 Nov 29, 2022
simple multi-threaded port scanner written in rust

knockson simple multi-threaded port scanner written in rust Install Using AUR https://aur.archlinux.org/packages/knockson-bin/ yay -Syu knockson-bin M

Josh Münte 4 Oct 5, 2022
Rust TLS/SSL certificate expiration date from command-line checker

Rust TLS/SSL certificate expiration date from command-line checker

Jose Bovet Derpich 9 Nov 9, 2022
Lightweight slowloris (HTTP DoS) implementation in Rust.

slowlorust Lightweight slowloris (HTTP DoS) implementation in Rust. Slowloris is a denial-of-service attack program which allows an attacker to overwh

Michael Van Leeuwen 6 Sep 29, 2022
A simple port scanner built using rust-lang

A simple port scanner built using rust-lang

Krisna Pranav 1 Nov 6, 2021
Safe Rust interface to the Vulkan API.

Magma: A strictly typed Vulkan API interface. Magma is a strictly typed Rust interface for the vulkan API. This means that whenever possible, the well

null 1 Oct 11, 2022