3 ms·

Hi nickpsecurity, I always like your posts, that's why I bookmarked your comments page and check it every few days for changes. What stands out, that these pap

Hi nickpsecurity, I always like your posts, that's why I bookmarked your comments page and check it every few days for changes. What stands out, that these papers and articles are pretty old. It seems to me that these are pretty academic examples. I don't understand why we can't see a lot of software in the wild, following the state of the art practices of building secure software. Maybe these practices are still relatively impracticable to the average programmer. Maybe research on secure software development should check their ideas more for psychological acceptability (Saltzer/Schröder).

nickpsecurity 9y ago
Glad you enjoy it. If you like that kind of stuff, you should keep an eye on Lobste.rs since I submit most of the CompSci stuff there. Mainly because they like it more over there but some people occasionally build on it. Mostly about formal methods filtered down to most interesting work but also do other stuff here and there. Here's a link to my submissions if you want to go through them: https://lobste.rs/newest/nickpsecurity https://lobste.rs/newest/nickpsecurity Far as old, it's important to remember that many things we're doing today started in some form a long time ago. Certain principles are timeless. For instance, the Burroughs B5000 was checking for overflows and argument matching on every operation at the CPU level back in 1961. That thing was immune to common, coding attacks until maybe when ROP was invented. The newer thing was C language designed for efficiency on weaker hardware. People still argue today if we can defeat the vulnerabilities in our legacy systems without realizing some in 60's-80's were immune to them. Occasionally, a current team will learn from or reinvent that older research to find it's still useful like crash-safe.org and Cambridge's CHERI did for secure CPU's w/ CHERI running FreeBSD. So, don't judge by age: look at what was done, why it worked, why it would/wouldn't today, if changes in context matter, and esp how practical it might be. Far as that, Cleanroom worked even on first try on real projects for commercial teams and students. I just got the book recently where I'll be trying it sometime in near future. It looks pretty good so far with it just being careful structuring and thinking about things in algebraic way. Why did it disappear? Likely bandwagon effect where some New Great Method got popular like it did, displaced it as project managers wanted to look like they were doing something new, and now it's a relic of history. Lots of stuff like that. Happens more if there's big companies with enterprise tooling backing the newcomers like the 4GL's, UML, etc. Even more when tool promises to remove human from equation as much as possible vs Cleanroom that built on human talent (i.e. time). Now, SPARK is entirely different. I got that book, too. :) It was always marketed at a niche group of people building stuff that should never fail. They have to be willing to spend a lot of time using specialist techniques to make that happen. They also must do it in non-mainstream language with proprietary tooling. Needless to say, adoption was small. However, AdaCore's site shows quite a few companies are using it in safety-critical work. I also have some case studies in my Lobsters submissions involving SPARK with keywords being "SPARK," "glider," and "cubesat" if you want to try to just Google them. Altran Praxis, who originally developed it, has been using it in government and commercial projects for one or two decades. The book supposedly makes it easier. I figure a combo of spec-based tests, automated solving, and runtime checks for what's left is still gonna be easiest approach. Aside from those two, another nice example is Design-by-Contract which is quite accessible to average developer. It just says what the component expects to receive, maintain, and deliver. That can be turned into tests, runtime checks, or verification conditions for a prover. One can also combine the runtime checks with fuzzing like AFL to make it zero in on the specific error. Eiffel Method brought that to significant adoption in industry even though small in larger scheme of things. We have seen increased adoption of some of those principles with more contract implementations in mainstream languages and property-based testing getting popular. Anyway, here's a nice description of that I saved as much for managers as developers: https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-by-contract/index.html https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b... "Maybe research on secure software development should check their ideas more for psychological acceptability (Saltzer/Schröder)." Oh, I've learned so much about this angle. I couldn't begin to tell you. Mostly pessimistic but there's some hope. We've been solving the wrong problems. Most of the security problem comes from political maneuverings through lobbyists, market preferences which rarely value security, and business incentives that are similar. There's strategies for each which have potential. My best hypothesis for now is to keep pushing methods that are productive with the tech designed for verification [later] with lightweight methods used up front. You sell the approach as much as possible on non-security benefits with a certain amount of money funneled into improving security of the project or its dependencies. Rinse repeat. Also, better to invest in projects that improve security on things with same language, API, ISA, etc as things with huge, bandwagon effects. Gotta go with the flow.

nickpsecurity 9y ago

Glad you enjoy it. If you like that kind of stuff, you should keep an eye on Lobste.rs since I submit most of the CompSci stuff there. Mainly because they like it more over there but some people occasionally build on it. Mostly about formal methods filtered down to most interesting work but also do other stuff here and there. Here's a link to my submissions if you want to go through them: https://lobste.rs/newest/nickpsecurity https://lobste.rs/newest/nickpsecurity Far as old, it's important to remember that many things we're doing today started in some form a long time ago. Certain principles are timeless. For instance, the Burroughs B5000 was checking for overflows and argument matching on every operation at the CPU level back in 1961. That thing was immune to common, coding attacks until maybe when ROP was invented. The newer thing was C language designed for efficiency on weaker hardware. People still argue today if we can defeat the vulnerabilities in our legacy systems without realizing some in 60's-80's were immune to them. Occasionally, a current team will learn from or reinvent that older research to find it's still useful like crash-safe.org and Cambridge's CHERI did for secure CPU's w/ CHERI running FreeBSD. So, don't judge by age: look at what was done, why it worked, why it would/wouldn't today, if changes in context matter, and esp how practical it might be. Far as that, Cleanroom worked even on first try on real projects for commercial teams and students. I just got the book recently where I'll be trying it sometime in near future. It looks pretty good so far with it just being careful structuring and thinking about things in algebraic way. Why did it disappear? Likely bandwagon effect where some New Great Method got popular like it did, displaced it as project managers wanted to look like they were doing something new, and now it's a relic of history. Lots of stuff like that. Happens more if there's big companies with enterprise tooling backing the newcomers like the 4GL's, UML, etc. Even more when tool promises to remove human from equation as much as possible vs Cleanroom that built on human talent (i.e. time). Now, SPARK is entirely different. I got that book, too. :) It was always marketed at a niche group of people building stuff that should never fail. They have to be willing to spend a lot of time using specialist techniques to make that happen. They also must do it in non-mainstream language with proprietary tooling. Needless to say, adoption was small. However, AdaCore's site shows quite a few companies are using it in safety-critical work. I also have some case studies in my Lobsters submissions involving SPARK with keywords being "SPARK," "glider," and "cubesat" if you want to try to just Google them. Altran Praxis, who originally developed it, has been using it in government and commercial projects for one or two decades. The book supposedly makes it easier. I figure a combo of spec-based tests, automated solving, and runtime checks for what's left is still gonna be easiest approach. Aside from those two, another nice example is Design-by-Contract which is quite accessible to average developer. It just says what the component expects to receive, maintain, and deliver. That can be turned into tests, runtime checks, or verification conditions for a prover. One can also combine the runtime checks with fuzzing like AFL to make it zero in on the specific error. Eiffel Method brought that to significant adoption in industry even though small in larger scheme of things. We have seen increased adoption of some of those principles with more contract implementations in mainstream languages and property-based testing getting popular. Anyway, here's a nice description of that I saved as much for managers as developers: https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-by-contract/index.html https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b... "Maybe research on secure software development should check their ideas more for psychological acceptability (Saltzer/Schröder)." Oh, I've learned so much about this angle. I couldn't begin to tell you. Mostly pessimistic but there's some hope. We've been solving the wrong problems. Most of the security problem comes from political maneuverings through lobbyists, market preferences which rarely value security, and business incentives that are similar. There's strategies for each which have potential. My best hypothesis for now is to keep pushing methods that are productive with the tech designed for verification [later] with lightweight methods used up front. You sell the approach as much as possible on non-security benefits with a certain amount of money funneled into improving security of the project or its dependencies. Rinse repeat. Also, better to invest in projects that improve security on things with same language, API, ISA, etc as things with huge, bandwagon effects. Gotta go with the flow.