4 ms·

> Makes it funny they're so worried about bringing CIA in. Except for the fact that the USG actually buys into the concept of NOBUS, as evidenced not only in t

by woodman 10y ago

> Makes it funny they're so worried about bringing CIA in. Except for the fact that the USG actually buys into the concept of NOBUS, as evidenced not only in the classification system - but also foreign policy (the proliferation of AA and AT weapons comes to mind). So the USG's use of TOR provides me with zero confidence that they wouldn't actively weaken it. That said, I agree on the issue of trust - secure software shouldn't need any. They need to decide between two very distinct paths: accept the insecurity and try to control it socially (no CIA guys), or mathematically demonstrate infallibility. Because one is so hard, and the inevitable failure of the other can be ignored for now - I'm guessing that we'll see no push for formal verification :)

nickpsecurity 10y ago
Was looking forward to see what you'd say here. :) "Except for the fact that the USG actually buys into the concept of NOBUS" This is true. I considered it given a subverted, but otherwise working, Tor network would be a win-win if CIA was subjected to pressure or wanted to de-anonymize opponents. Yet, the Tor project themselves answer this one: it's vulnerable to a global, passive adversary. NSA has painstakingly built partnerships with all kinds of countries that collectively do a giant SIGINT operation. Most of them probably don't like Tor. CIA or partners can get info from NSA on these things. So, CIA can already defeat Tor for some fraction of users since their partner is outside its probability of success. On top of whatever CIA might pull. "accept the insecurity and try to control it socially (no CIA guys), or mathematically demonstrate infallibility. " Well, remember that there's always the path of just clearly specifying the functionality plus implementing it in the safest way possible. We used to call this medium assurance. OpenBSD is the code-only version of that. Praxis w/ Ada/SPARK is the spec + code version. Only around 30-50% premium in labor/cost added doing these things despite immunity to all kinds of shit. They aren't going to do it, though. They never do. Leading to... "I'm guessing that we'll see no push for formal verification :)" ...no push for that or even system-oriented languages and techniques that make the service immune to memory- or interface-level attacks that make up 80-90% of vulnerabilities. Not even that.
- woodman 10y ago
  We certainly share an interest. > Yet, the Tor project themselves answer this one: it's vulnerable to a global, passive adversary. Vulnerable to traffic analysis, I'm sure certain organizations wouldn't mind seeing that vulnerability include cleartext. > ...plus implementing it in the safest way possible. I've never seen an Underhanded Ada Contest, but I'm pretty confident that a bad actor could still introduce vulnerabilities that would pass a reasonable code review and be deniable. It would be an improvement for sure, but you'd still have a trust requirement. I think a good half measure would be: fully spec'd pure functions don't need human code review - just feed patches to the theorem prover and regression tester, all the trusted human labor can then focus on things that touch global state. At the risk of incentivizing spaghetti code, you'd incentivize the production of code that really lends itself to static analysis. > ...memory- or interface-level attacks that make up 80-90% of vulnerabilities. I look forward to us getting past the memory vulnerabilities, but the next battle will be one hell of a fight - timing attacks. Thought getting people to trade C performance was tough? Try getting them to intentionally delay all comparison operations... in the entire software stack :)
  - nickpsecurity 10y ago
    "Vulnerable to traffic analysis, I'm sure certain organizations wouldn't mind seeing that vulnerability include cleartext." Well, certainly. Depends on what this guy's role is supposed to be in the organization. One can always relegate the riskier people to stuff that can't harm them much. In any case, NSA can already do what you mentioned given leaks mention active targeting. Catalog includes regular malware, 0-days on stuff, and implants. Tor is the LTD they aim at themselves with optional LGB's following from QUANTUM and such. So, it would be a matter of already-vulnerable people or services getting more so. "I've never seen an Underhanded Ada Contest, but I'm pretty confident that a bad actor could still introduce vulnerabilities that would pass a reasonable code review and be deniable" Well, sure. Just remember, though, that what you're saying already applies to the Tor project. Any of the contributors, maintainers, relay hosts, and so on might be malicious. That's why A1 class called for protection throughout whole lifecycle which my framework below expanded on. SAP security guides showed most areas requiring protection. Examples below: http://pastebin.com/y3PufJ0V http://pastebin.com/y3PufJ0V http://www.dss.mil/documents/odaa/nispom2006-5220.pdf http://www.dss.mil/documents/odaa/nispom2006-5220.pdf Now, from here, we have to ask what can be done to mitigate potential exploits. Well, we know the protocol itself is subject to strong, peer review by parties more than willing to publish problems and organization that corrects them. The main problems occur in crypto libraries, protocol engines, interfaces, type checks, memory errors, parsing, handling time, and error handling. A type-safe, memory-safe, low-level language along lines of Ada/SPARK, Go, Rust, or Modula-3 plus specific libraries and guidance on aforementioned can knock out vast majority of the risk. Well, that along with parser/protocol generators already available in academia with hand-checked code and design-by-contract to encode constraints. OpenBSD people probably do considerably more work on their code than what would be necessary to take care of this in safer language while focusing on areas most likely to be hit. So, I think we can get plenty mileage without full, formal verification. There will be flaws just as there are in protocol itself. Yet, it will work most of the time with people finding problems so long as plenty are on it motivated to do so. " I think a good half measure would be: fully spec'd pure functions don't need human code review - just feed patches to the theorem prover and regression tester, all the trusted human labor can then focus on things that touch global state." They still need review. You have to specify what you're going to do, what security properties it maintains, how it maintains that, and the implementation correspondence. Usually also show compiler didn't screw it up. That's tricky. Pure functions are fine but covert channel analysis means it's going to be an imperative language for final implementation. Old model was basically decomposing functional components into state machines representing every permissible state. Can check by eye that they either should work securely or fail-safe. Still keeping my eye out for CompSci tech that can derive imperative from simple, functional languages in human-readable form. "Thought getting people to trade C performance was tough? Try getting them to intentionally delay all comparison operations... in the entire software stack :)" Oh my god, I've been there. Mainstream INFOSEC totally ignored that problem saying it was unnecessary until recently rediscovering it under "side channel" label. Running wild with it. I called out Freenet on Schneier's blog as probably having plenty due to use of Java. Meanwhile, old methods of handling timing channels were reducing precision, fixed-rate, maximum-time, turning off caches (extra painful on Core i7), masking, and my favorite being asynchronous, randomized execution. I was going to put the latter in a CPU then found someone else already did that. Clever. Partitioned caches are another popular strategy. I just stick with Red/Black model in my designs with trusted part being dedicated chip with timing mitigation for just needed part. Still performance hit no matter what. Anyway, I did a write-up for someone on how to secure a service like Tor here: https://www.schneier.com/blog/archives/2014/09/identifying_dre.html#c6678915 https://www.schneier.com/blog/archives/2014/09/identifying_d...

by woodman 10y ago

nickpsecurity 10y ago

Was looking forward to see what you'd say here. :) "Except for the fact that the USG actually buys into the concept of NOBUS" This is true. I considered it given a subverted, but otherwise working, Tor network would be a win-win if CIA was subjected to pressure or wanted to de-anonymize opponents. Yet, the Tor project themselves answer this one: it's vulnerable to a global, passive adversary. NSA has painstakingly built partnerships with all kinds of countries that collectively do a giant SIGINT operation. Most of them probably don't like Tor. CIA or partners can get info from NSA on these things. So, CIA can already defeat Tor for some fraction of users since their partner is outside its probability of success. On top of whatever CIA might pull. "accept the insecurity and try to control it socially (no CIA guys), or mathematically demonstrate infallibility. " Well, remember that there's always the path of just clearly specifying the functionality plus implementing it in the safest way possible. We used to call this medium assurance. OpenBSD is the code-only version of that. Praxis w/ Ada/SPARK is the spec + code version. Only around 30-50% premium in labor/cost added doing these things despite immunity to all kinds of shit. They aren't going to do it, though. They never do. Leading to... "I'm guessing that we'll see no push for formal verification :)" ...no push for that or even system-oriented languages and techniques that make the service immune to memory- or interface-level attacks that make up 80-90% of vulnerabilities. Not even that.

woodman 10y ago
We certainly share an interest. > Yet, the Tor project themselves answer this one: it's vulnerable to a global, passive adversary. Vulnerable to traffic analysis, I'm sure certain organizations wouldn't mind seeing that vulnerability include cleartext. > ...plus implementing it in the safest way possible. I've never seen an Underhanded Ada Contest, but I'm pretty confident that a bad actor could still introduce vulnerabilities that would pass a reasonable code review and be deniable. It would be an improvement for sure, but you'd still have a trust requirement. I think a good half measure would be: fully spec'd pure functions don't need human code review - just feed patches to the theorem prover and regression tester, all the trusted human labor can then focus on things that touch global state. At the risk of incentivizing spaghetti code, you'd incentivize the production of code that really lends itself to static analysis. > ...memory- or interface-level attacks that make up 80-90% of vulnerabilities. I look forward to us getting past the memory vulnerabilities, but the next battle will be one hell of a fight - timing attacks. Thought getting people to trade C performance was tough? Try getting them to intentionally delay all comparison operations... in the entire software stack :)
- nickpsecurity 10y ago
  "Vulnerable to traffic analysis, I'm sure certain organizations wouldn't mind seeing that vulnerability include cleartext." Well, certainly. Depends on what this guy's role is supposed to be in the organization. One can always relegate the riskier people to stuff that can't harm them much. In any case, NSA can already do what you mentioned given leaks mention active targeting. Catalog includes regular malware, 0-days on stuff, and implants. Tor is the LTD they aim at themselves with optional LGB's following from QUANTUM and such. So, it would be a matter of already-vulnerable people or services getting more so. "I've never seen an Underhanded Ada Contest, but I'm pretty confident that a bad actor could still introduce vulnerabilities that would pass a reasonable code review and be deniable" Well, sure. Just remember, though, that what you're saying already applies to the Tor project. Any of the contributors, maintainers, relay hosts, and so on might be malicious. That's why A1 class called for protection throughout whole lifecycle which my framework below expanded on. SAP security guides showed most areas requiring protection. Examples below: http://pastebin.com/y3PufJ0V http://pastebin.com/y3PufJ0V http://www.dss.mil/documents/odaa/nispom2006-5220.pdf http://www.dss.mil/documents/odaa/nispom2006-5220.pdf Now, from here, we have to ask what can be done to mitigate potential exploits. Well, we know the protocol itself is subject to strong, peer review by parties more than willing to publish problems and organization that corrects them. The main problems occur in crypto libraries, protocol engines, interfaces, type checks, memory errors, parsing, handling time, and error handling. A type-safe, memory-safe, low-level language along lines of Ada/SPARK, Go, Rust, or Modula-3 plus specific libraries and guidance on aforementioned can knock out vast majority of the risk. Well, that along with parser/protocol generators already available in academia with hand-checked code and design-by-contract to encode constraints. OpenBSD people probably do considerably more work on their code than what would be necessary to take care of this in safer language while focusing on areas most likely to be hit. So, I think we can get plenty mileage without full, formal verification. There will be flaws just as there are in protocol itself. Yet, it will work most of the time with people finding problems so long as plenty are on it motivated to do so. " I think a good half measure would be: fully spec'd pure functions don't need human code review - just feed patches to the theorem prover and regression tester, all the trusted human labor can then focus on things that touch global state." They still need review. You have to specify what you're going to do, what security properties it maintains, how it maintains that, and the implementation correspondence. Usually also show compiler didn't screw it up. That's tricky. Pure functions are fine but covert channel analysis means it's going to be an imperative language for final implementation. Old model was basically decomposing functional components into state machines representing every permissible state. Can check by eye that they either should work securely or fail-safe. Still keeping my eye out for CompSci tech that can derive imperative from simple, functional languages in human-readable form. "Thought getting people to trade C performance was tough? Try getting them to intentionally delay all comparison operations... in the entire software stack :)" Oh my god, I've been there. Mainstream INFOSEC totally ignored that problem saying it was unnecessary until recently rediscovering it under "side channel" label. Running wild with it. I called out Freenet on Schneier's blog as probably having plenty due to use of Java. Meanwhile, old methods of handling timing channels were reducing precision, fixed-rate, maximum-time, turning off caches (extra painful on Core i7), masking, and my favorite being asynchronous, randomized execution. I was going to put the latter in a CPU then found someone else already did that. Clever. Partitioned caches are another popular strategy. I just stick with Red/Black model in my designs with trusted part being dedicated chip with timing mitigation for just needed part. Still performance hit no matter what. Anyway, I did a write-up for someone on how to secure a service like Tor here: https://www.schneier.com/blog/archives/2014/09/identifying_dre.html#c6678915 https://www.schneier.com/blog/archives/2014/09/identifying_d...