3 ms·

Neat, but unless I am missing something, a nightmare in terms of security. Assembly has a worse type system than even C: essentially no type system at all! (Or

by anyfoo 8y ago

Neat, but unless I am missing something, a nightmare in terms of security. Assembly has a worse type system than even C: essentially no type system at all! (Or rather the weakest, simplest, most dynamic type system you can imagine.)

nickpsecurity 8y ago
There has been a lot of work on that. Look up Typed Assembly Language, Security in front of that, and Dependently-Typed Assembly Language. Here's one that was integrated with a safe, C variant. https://www.cs.cornell.edu/talc/ https://www.cs.cornell.edu/talc/
- anyfoo 8y ago
  Wow, even dependently typed, that's pretty brilliant. I can see this being enormously helpful when writing very low level, for example early boot stage, assembly code.
- ChickeNES 8y ago
  Unfortunately it appears that the linked project is not free software :(
  - nickpsecurity 8y ago
    I have the source but you're right: no obvious license file. I might email them about it.
userbinator 8y ago
On the other hand, there is essentially no undefined behaviour, no chances of compiler bugs/backdoors, and the code is (by necessity) simple enough that what it does can be easily analysed and understood. Not a lot of places for bugs, security or otherwise, to hide if there's not a lot of code in the first place.
- nickpsecurity 8y ago
  "no chances of compiler bugs/backdoors" That's not true if running complex assembly through an assembler and/or linker. Aside from totally changing the program, there's definitely potential for it to be modified to do things like drop safety checks for optimizations or use instruction patterns that increase covert channels. That's on top of not working correctly at all. I'll add to that point that the Intel documentation is huge with every processor having errata. That's why high-assurance security always considers those things inside the Trusted Computing Base (TCB).
  - acqq 8y ago
    > there's definitely potential for it to be modified to do things like drop safety checks for optimizations Can you please give some link? It sounds strange, I’ve never read about something like that happening in assembly (“drop safety checks for optimization” — which checks, how can that even happen? Maybe you confused that with the writings about what C compilers do?).
    - nickpsecurity 8y ago
      Well, let me first say how high-assurance security makes us think on these things: everything is incorrect, insecure, and backdoored by design until proven otherwise. Then, there's rigorous methods for attempting to prove otherwise. We also try to speculate about attacks using a mix of prior attacks (known knowns) and variations of prior problems (known unknowns). So, here's a few things that came to my mind: The assembler or linker are programmed to look for and drop checks for stuff like buffer overflow. A "macro" assembler has some code generation. It might generate the code in an insecure way. An malicious assembler might swap out instructions that prevent side channels for equivalent instructions that cause them. There's lots of ways to screw up assembly code in general on correctness side that might at least lead to DOS. The malicious assembler might do any of them. The linker might do any of that. It could even be a better place for it since few people understand or look at linkers. Although memory is fuzzy right now, you could also look for any security errors that started with the linker. They could be done on purpose. So, I would expect a formal specification of each component, their correctness/safety/security requirements (policy), the implementation, and evidence the implementation maintains the spec and policy. CompCert and CakeML are example compilers that do that for correctness. I can't recall if someone verified a x86 assembler and linker. Rockwell-Collins is best example of your CPU/microcode being verified in itself and against specs of your application code function by function. I've also seen formal work on linking, mainly with type systems, in Standard ML that a lot of proof systems output. Most just ignore assemblers and linkers for x86 for some reason. Be a great project for some people to jump on! :) http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf

by anyfoo 8y ago

nickpsecurity 8y ago

There has been a lot of work on that. Look up Typed Assembly Language, Security in front of that, and Dependently-Typed Assembly Language. Here's one that was integrated with a safe, C variant. https://www.cs.cornell.edu/talc/ https://www.cs.cornell.edu/talc/

anyfoo 8y ago
Wow, even dependently typed, that's pretty brilliant. I can see this being enormously helpful when writing very low level, for example early boot stage, assembly code.
ChickeNES 8y ago
Unfortunately it appears that the linked project is not free software :(
- nickpsecurity 8y ago
  I have the source but you're right: no obvious license file. I might email them about it.

userbinator 8y ago

On the other hand, there is essentially no undefined behaviour, no chances of compiler bugs/backdoors, and the code is (by necessity) simple enough that what it does can be easily analysed and understood. Not a lot of places for bugs, security or otherwise, to hide if there's not a lot of code in the first place.

nickpsecurity 8y ago
"no chances of compiler bugs/backdoors" That's not true if running complex assembly through an assembler and/or linker. Aside from totally changing the program, there's definitely potential for it to be modified to do things like drop safety checks for optimizations or use instruction patterns that increase covert channels. That's on top of not working correctly at all. I'll add to that point that the Intel documentation is huge with every processor having errata. That's why high-assurance security always considers those things inside the Trusted Computing Base (TCB).
- acqq 8y ago
  > there's definitely potential for it to be modified to do things like drop safety checks for optimizations Can you please give some link? It sounds strange, I’ve never read about something like that happening in assembly (“drop safety checks for optimization” — which checks, how can that even happen? Maybe you confused that with the writings about what C compilers do?).
  - nickpsecurity 8y ago
    Well, let me first say how high-assurance security makes us think on these things: everything is incorrect, insecure, and backdoored by design until proven otherwise. Then, there's rigorous methods for attempting to prove otherwise. We also try to speculate about attacks using a mix of prior attacks (known knowns) and variations of prior problems (known unknowns). So, here's a few things that came to my mind: The assembler or linker are programmed to look for and drop checks for stuff like buffer overflow. A "macro" assembler has some code generation. It might generate the code in an insecure way. An malicious assembler might swap out instructions that prevent side channels for equivalent instructions that cause them. There's lots of ways to screw up assembly code in general on correctness side that might at least lead to DOS. The malicious assembler might do any of them. The linker might do any of that. It could even be a better place for it since few people understand or look at linkers. Although memory is fuzzy right now, you could also look for any security errors that started with the linker. They could be done on purpose. So, I would expect a formal specification of each component, their correctness/safety/security requirements (policy), the implementation, and evidence the implementation maintains the spec and policy. CompCert and CakeML are example compilers that do that for correctness. I can't recall if someone verified a x86 assembler and linker. Rockwell-Collins is best example of your CPU/microcode being verified in itself and against specs of your application code function by function. I've also seen formal work on linking, mainly with type systems, in Standard ML that a lot of proof systems output. Most just ignore assemblers and linkers for x86 for some reason. Be a great project for some people to jump on! :) http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf