3 ms·
Can you elaborate as to how to prevent use-after-free statically in C without forbidding dynamic memory allocation?
by pcwalton 9y ago
Can you elaborate as to how to prevent use-after-free statically in C without forbidding dynamic memory allocation?
- Nokinside 9y agoBy proving that memory references don't live longer than the allocated memory. The use of dynamic allocation must be carefully restricted and programmer may need to provide provide assertions or modify the code to pass verification. There is two ways tho think static verification: 1. Language level verification. All valid programs are verified to be correct in respect of safety guarantees the language gives. 2. Verification of safety features that can't be proved in general. In most cases it's possible to write program in a way that it can be verified to be correct, but finding a way to write provably correct program may need some work.
- pjmlp 9y agoNow try to use that in the presence of commercial libraries.
- jhasse 9y agoTry to use Rust in the presence of commercial libraries.
- pjmlp 9y agoEasy just like any compiler for a memory safe language. There might exist logical bugs, but the language semantics allow for a higher thrust of code quality, assuming the binaries haven't been tampered with. Every line of C code is unsafe, specially if the binary was compiled with -O3. Regarding Rust, the only issue is lack of support for binary libraries in Cargo, one needs to call rustc directly.
- Rusky 9y agoLinux doesn't do any of this, and doing so is tantamount to running a borrow checker on the code, which requires more information than is present in vanilla C.
- pcwalton 9y agoAt that point you will have basically reinvented Rust. The resulting language will be so incompatible as to essentially be a new language.
- fpoling 9y agoA static checker for C code can do the similar checks that the borrow checker in Rust does. Essentially it enforces a variation of linear type system. Note that many things for Rust are on ideas from Cyclone [1], that was a research project to provide minimal extensions to C type system to ensure memory safety. [1] - https://cyclone.thelanguage.org/ https://cyclone.thelanguage.org/
- pjmlp 9y agoOnly works if 100% of the code is available, thus not usable by companies selling commercial libraries.
- fpoling 9y agoStatic checker can work in principle on binary code. Alternatively, one can annotate API the library provides for the static checker. This is especially feasible with C where API types and usage is typically rather simple. Clearly, this implies trusting API to be implemented correctly or at least using the static checker to prove that memory-safety bugs are originated in the library, not in the application code.
- jcelerier 9y agoThat's not really relevant when talking about the linux kernel, though, is it ? There's tons and tons of open-source code that could just run clang-analyze today and eliminate swathes of memory bugs.
- pjmlp 9y agoSure it is, starting by the GPU drivers.
- pcwalton 9y agoI read the Cyclone papers when I designed the original Rust borrow checker, and we spoke to Dan Grossman. Cyclone only works because it uses garbage collection for the heap. There is a uniqueness extension, but it is limited compared to what Rust can do. (See Grossman's "Existential Types for Imperative Languages" presentation for details.) The uniqueness extension was not designed to (and is not flexible enough to) supplant the garbage collector in most real-world projects. This theoretical static checker for C code would not be compatible with virtually any existing C code in the wild, and so it would be effectively a new language.