4 ms·

>this take doesn’t make any sense having small amount of unsafe primitives is not the same as having all of your code unsafe I've been arguing this for years.

by carlmr 2y ago

>this take doesn’t make any sense having small amount of unsafe primitives is not the same as having all of your code unsafe I've been arguing this for years. It makes the area you need to review more tightly much smaller. Making it way easier to find bugs in the first place. I'm sometimes wondering if unsafe was the right choice of keyword. Because to people that don't understand the language, it conveys the sense that Rust doesn't help with memory safety at all. I've written a bunch of Rust, and rarely needed to use unsafe. I'd say less than 0.1% of the lines written. Aside from that unsafe Rust still has a lot more safety precautions than standard C++. It doesn't even deactivate the borrow checker. [1] [1] https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html

nickpsecurity 2y ago
In the past, safe vs unsafe meant whether it preserved invariants in all executions of your code. Was your code type- and memory-safe by default in all situations? Was there a guarantee? If so, it was safe. If breaking that guarantee or outside the type system, it was “unsafe.” Note: I don’t know enough about Rust to tell you how they should label it. Another thing you might find interesting is external verification of unsafe modules. What you do is build static analyzers, verifiers, etc that can prove the absence of entire categories of bugs, esp memory safety. It’s usually for small code. You run that on the code that doesn’t use memory safety. Another technique is making a verified, reference implementation that’s used to confirm the high-performance implementation. Their interfaces and structure are designed to match. Then, automated methods for equivalence checking verify the unsafe code matches the safe code in all observed cases. The equivalence might be formal and/or test generators. You can also wrap the unsafe code in safe interfaces that force it to be used correctly. I imagine the Rust TLS does this to some degree. Projects like miTLS go further to enforce specific, security properties during interactions between verified and unsafe code. The last thing to consider are abstraction gap attacks. If mixing languages or models, then the behavior of one can make the other unsafe just because they work differently. Especially in how the compiler structures or links them. This led to real vulnerabilities in Ada code that used C just due to interactions, not the C code. Although previously checked by eye, there’s a new field called secure compilation or abstract compilation trying to eliminate the integration vulnerabilities. Lastly, if not too bad for performance, some sandboxed the unsafe code with the interfaces checking communication both ways. Techniques used include processes (seL4), segments (GEMSOS), capabilities (CHERI), and physical (FPGA coprocessors). It’s usually performance-prohibitive to separate crypto primitives like this. Whereas, coprocessors can have verified crypto and be faster, though. (See Cryptol-generated VHDL.)

by carlmr 2y ago

nickpsecurity 2y ago

In the past, safe vs unsafe meant whether it preserved invariants in all executions of your code. Was your code type- and memory-safe by default in all situations? Was there a guarantee? If so, it was safe. If breaking that guarantee or outside the type system, it was “unsafe.” Note: I don’t know enough about Rust to tell you how they should label it. Another thing you might find interesting is external verification of unsafe modules. What you do is build static analyzers, verifiers, etc that can prove the absence of entire categories of bugs, esp memory safety. It’s usually for small code. You run that on the code that doesn’t use memory safety. Another technique is making a verified, reference implementation that’s used to confirm the high-performance implementation. Their interfaces and structure are designed to match. Then, automated methods for equivalence checking verify the unsafe code matches the safe code in all observed cases. The equivalence might be formal and/or test generators. You can also wrap the unsafe code in safe interfaces that force it to be used correctly. I imagine the Rust TLS does this to some degree. Projects like miTLS go further to enforce specific, security properties during interactions between verified and unsafe code. The last thing to consider are abstraction gap attacks. If mixing languages or models, then the behavior of one can make the other unsafe just because they work differently. Especially in how the compiler structures or links them. This led to real vulnerabilities in Ada code that used C just due to interactions, not the C code. Although previously checked by eye, there’s a new field called secure compilation or abstract compilation trying to eliminate the integration vulnerabilities. Lastly, if not too bad for performance, some sandboxed the unsafe code with the interfaces checking communication both ways. Techniques used include processes (seL4), segments (GEMSOS), capabilities (CHERI), and physical (FPGA coprocessors). It’s usually performance-prohibitive to separate crypto primitives like this. Whereas, coprocessors can have verified crypto and be faster, though. (See Cryptol-generated VHDL.)