7 ms·

Thanks for the Rockwell-Collins link! What I understand there verified is however not that the adversary can't add malicious code but that there are formal ver

by acqq 8y ago

Thanks for the Rockwell-Collins link! What I understand there verified is however not that the adversary can't add malicious code but that there are formal verification steps that no bugs are introduced as the non-subverted implementation is introduced. I agree with you that the linkers are a nice place for the malicious code to be hidden. The malicious code can be anywhere in practice... the way I see it, the accidental errors that introduce security issues are much more probable in compilers and the modern linkers (especially as they do more of a job that formerly only compilers did) than in assemblers. The assemblers are surely the easiest to be verified on producing what is expected of them to produce: a separately developed disassembler is enough.

nickpsecurity 8y ago
"What I understand there verified is however not that the adversary can't add malicious code but that there are formal verification steps that no bugs are introduced as the non-subverted implementation is introduced." What they did is a high-level view (formal spec) of exactly what it does, one of what it means to be secure, and proof the design matches that. It's harder to subvert. It can also prove the system can't be attacked if they model those properties. For instance, they do show some protection against leaks from one process to another with the non-interference property of their partitioning mechanism. I just posted a lot more stuff like that in hardware and software here if you're interested: https://news.ycombinator.com/item?id=17530829 https://news.ycombinator.com/item?id=17530829 " the way I see it, the accidental errors that introduce security issues are much more probable in compilers and the modern linkers (especially as they do more of a job that formerly only compilers did) than in assemblers." I agree. I bring it up every time someone erroneously focuses on the Karger/Thompson attack on compilers. The more common error is the compiler messing the code up. An easier subversion would be to put a bug into a compiler that did that which looked like a normal bug. It's why certifying compilers are necessary. Note that TALC is part of a bigger picture at FLINT team where they do certifying compilers for stuff like ML, safe versions of C, intermediate/assembly languages that are typed for extra layer of defense, I/O, interrupts, and many other things. Here's their work: http://flint.cs.yale.edu/flint/publications/ http://flint.cs.yale.edu/flint/publications/ http://flint.cs.yale.edu/flint/software.html http://flint.cs.yale.edu/flint/software.html Yeah, assemblers should be pretty easy if they're just doing straight-forward stuff preserving the data and structure. Those like Hyde's High-Level Assembly (HLA) might be trickier with high-level functionality. However, even those might be divided between a first-pass acting as a compiler for high-level stuff and a simpler assembler.

by acqq 8y ago

nickpsecurity 8y ago

"What I understand there verified is however not that the adversary can't add malicious code but that there are formal verification steps that no bugs are introduced as the non-subverted implementation is introduced." What they did is a high-level view (formal spec) of exactly what it does, one of what it means to be secure, and proof the design matches that. It's harder to subvert. It can also prove the system can't be attacked if they model those properties. For instance, they do show some protection against leaks from one process to another with the non-interference property of their partitioning mechanism. I just posted a lot more stuff like that in hardware and software here if you're interested: https://news.ycombinator.com/item?id=17530829 https://news.ycombinator.com/item?id=17530829 " the way I see it, the accidental errors that introduce security issues are much more probable in compilers and the modern linkers (especially as they do more of a job that formerly only compilers did) than in assemblers." I agree. I bring it up every time someone erroneously focuses on the Karger/Thompson attack on compilers. The more common error is the compiler messing the code up. An easier subversion would be to put a bug into a compiler that did that which looked like a normal bug. It's why certifying compilers are necessary. Note that TALC is part of a bigger picture at FLINT team where they do certifying compilers for stuff like ML, safe versions of C, intermediate/assembly languages that are typed for extra layer of defense, I/O, interrupts, and many other things. Here's their work: http://flint.cs.yale.edu/flint/publications/ http://flint.cs.yale.edu/flint/publications/ http://flint.cs.yale.edu/flint/software.html http://flint.cs.yale.edu/flint/software.html Yeah, assemblers should be pretty easy if they're just doing straight-forward stuff preserving the data and structure. Those like Hyde's High-Level Assembly (HLA) might be trickier with high-level functionality. However, even those might be divided between a first-pass acting as a compiler for high-level stuff and a simpler assembler.