|
1 |
| -# MIRAI [](https://codecov.io/gh/facebookexperimental/MIRAI) [](https://deps.rs/repo/github/facebookexperimental/MIRAI) |
| 1 | +# MIRAI |
| 2 | + |
2 | 3 | MIRAI is an abstract interpreter for the [Rust](https://www.rust-lang.org/) compiler's [mid-level intermediate
|
3 | 4 | representation](https://github.com/rust-lang/rfcs/blob/master/text/1211-mir.md) (MIR).
|
4 |
| -It is intended to become a widely used static analysis tool for Rust. |
5 |
| - |
6 |
| -## Request for Proposals |
7 |
| - |
8 |
| -The Web3 Foundation has an |
9 |
| -[RFP](https://github.com/w3f/Grants-Program/blob/master/docs/RFPs/Open/Static-Analysis-for-Runtime-Pallets.md) |
10 |
| -for extending MIRAI. If you are interested in making a proposal, feel free to do so and expect to count on support |
11 |
| -with design reviews, coding and merging your contributions. Contact [email protected] if you want to discuss this |
12 |
| -further. |
13 |
| - |
14 |
| -## Who should use MIRAI |
15 |
| - |
16 |
| -MIRAI can be used as a linter that finds panics that may be unintentional or are not the best way to terminate a |
17 |
| -program. This use case generally requires no annotations and is best realized by integrating MIRAI into a CI pipeline. |
18 |
| - |
19 |
| -MIRAI can also be used to verify correctness properties. Such properties need to be encoded into annotations of the |
20 |
| -source program. |
21 |
| - |
22 |
| -A related use is to better document an API via explicit precondition annotations and then use MIRAI to check that |
23 |
| -the annotations match the code. |
24 |
| - |
25 |
| -Finally, MIRAI can be used to look for security bugs via taint analysis (information leaks, code injection bugs, etc.) |
26 |
| -and constant time analysis (information leaks via side channels). Unintentional (or ill-considered) panics can also |
27 |
| -become security problems (denial of service, undefined behavior). |
28 |
| - |
29 |
| -## How to use MIRAI |
30 |
| - |
31 |
| -You'll need to install MIRAI as described |
32 |
| -[here](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/InstallationGuide.md). |
33 |
| - |
34 |
| -Then use `cargo mirai` to run MIRAI over your current package. This works much like `cargo check` but uses MIRAI rather |
35 |
| -than rustc to analyze the targets of your current package. |
36 |
| - |
37 |
| -`cargo mirai` does a top-down full-program path sensitive analysis of the |
38 |
| -[entry points](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/Overview.md#entry-points) of your |
39 |
| -package. To analyze test functions instead, use `cargo mirai --tests`. |
40 |
| - |
41 |
| -This will likely produce some warnings. Some of these will be real issues (true positives) that you'll fix by changing |
42 |
| -the offending code. Other warnings will be due to limitations of MIRAI and you can silence them by adding annotations |
43 |
| -declared in this [crate](https://crates.io/crates/mirai-annotations). |
44 |
| - |
45 |
| -Once MIRAI gives your code a clean bill of health, your code will be better documented and more readable. Perhaps you'll |
46 |
| -also have found and fixed a few bugs. |
47 |
| - |
48 |
| -You can use the environment variable `MIRAI_FLAGS` to get cargo to provide command line options to MIRAI. The value is a |
49 |
| -string which can contain any of the following flags: |
50 |
| - |
51 |
| -- `--diag=default|verify|library|paranoid`: configures level of diagnostics. With `default` MIRAI |
52 |
| - will not report errors which are potential 'false positives'. With `verify` it will point out |
53 |
| - functions that may contain such errors. With `library` it will require explicit preconditions. |
54 |
| - With `paranoid` it will flag any issue that may be an error. |
55 |
| -- `--single_func <name>`: the name of a specific function you want to analyze. |
56 |
| -- `--body_analysis_timeout <seconds>`: the maximum number of seconds to spend analyzing a function body. |
57 |
| -- `--call_graph_config <path_to_config>`: path to configuration file for call graph generator (see [Call Graph Generator documentation](documentation/CallGraph.md)). No call graph will be generated if this is not specified. |
58 |
| -- `--print_function_names`: just print the source location and fully qualified function signature of every function. |
59 |
| -- `--`: any arguments after this marker are passed on to rustc. |
60 |
| - |
61 |
| -You can get some insight into the inner workings of MIRAI by setting the verbosity level of log output to one of |
62 |
| -`warn`, `info`, `debug`, or `trace`, via the environment variable `MIRAI_LOG`. |
63 |
| - |
64 |
| -## Developing MIRAI |
65 |
| -See the [developer guide](https://github.com/facebookexperimental/MIRAI/blob/main/documentation//DeveloperGuide.md) |
66 |
| -for instructions on how to build, run and debug MIRAI. |
67 | 5 |
|
68 |
| -## Full documentation |
69 |
| -* [Overview of project](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/Overview.md). |
70 |
| -* [Architecture](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/Architecture.md). |
71 |
| -* [Design discussions](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/DesignDiscussions.md). |
72 |
| -* [Further reading](https://github.com/facebookexperimental/MIRAI/blob/main/documentation/FurtherReading.md). |
| 6 | +It started out as a Facebook project, but became orphaned when the sponsoring organization was disbanded. |
73 | 7 |
|
74 |
| -## Join the MIRAI community |
75 |
| -<!-- * Website: |
76 |
| -* Facebook page: |
77 |
| -* Mailing list |
78 |
| -* irc: --> |
79 |
| -See the [CONTRIBUTING](https://github.com/facebookexperimental/MIRAI/blob/main/CONTRIBUTING.md) file for how to help out. |
| 8 | +Ongoing work to keep the project alive now happens at https://github.com/endorlabs/MIRAI. |
80 | 9 |
|
81 |
| -## License |
82 |
| -MIRAI is MIT licensed, as found in the [LICENSE](https://github.com/facebookexperimental/MIRAI/blob/main/LICENSE) file. |
0 commit comments