[2212.12976] Modular Formal Verification of Rust Programs with Unsafe Blocks
source link: https://arxiv.org/abs/2212.12976
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
[Submitted on 26 Dec 2022]
Modular Formal Verification of Rust Programs with Unsafe Blocks
Rust is a modern systems programming language whose type system guarantees memory safety. For the sake of expressivity and performance it allows programmers to relax typing rules temporarily, using unsafe code blocks. However, in unsafe blocks, the burden of making sure that the code does not end up having undefined behaviour is on the programmer. Even most expert programmers make mistakes and a memory safety bug in an unsafe block renders all the type system guarantees void. To address this problem we are trying to verify soundness of Rust unsafe code applying our Modular Symbolic Execution algorithm. This text outlines our approach and the progress that has been made so far.
| Comments: | 22 pages, 13 listings, 3 figures, Technical report, Appendix by Bart Jacobs |
| Subjects: | Logic in Computer Science (cs.LO); Programming Languages (cs.PL) |
| Cite as: | arXiv:2212.12976 [cs.LO] |
| (or arXiv:2212.12976v1 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2212.12976 |
Recommend
-
32
We recently used the UCLID5 verifier, developed at U.C., Berkeley, to formally verify the Y86-64 processors described in Chapter 4 of CS:APP3e. You can get more information about UCLID5, as well as the verifier itself a...
-
13
In the summer of 2015 a team of hackers attempted to take control of an unmanned military helicopter known as Little Bird . The helicopter, which is...
-
12
Formal Verification of Smart Contracts with the K Framework Currently, blockchain technology is mostly used for handling investments and significant amounts of money. But vulnerabilities in smart contracts can allow hacke...
-
9
Conversation Copy link Contributor ...
-
9
Misspecification: The Blind Spot of Formal VerificationOctober 06, 2021As people, we like to be right, and we also want to avoid the effort of proving that we’re...
-
7
Copy link Contributor r00ster91
-
5
The Verification Gap: A Major Hurdle for the Industry Adoption of Formal MethodsJuly 12, 2022 Let’s assume that we’ve made...
-
4
Dr. David J. PearceFormal Verification of a Token ContractThursday, September 15th, 2022Following on from my previous post on
-
3
Systems & Design Formal Verification’s Usefulness Widens ...
-
7
Why fuzzing over formal verification? By Tarun Bansal, Gustavo Grieco, and Josselin Feist We recently introduced our new offering,
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK