Did not know about the answer/comment distinction! Thanks for pointing that out.
Before I dig deeper, I’d like to encourage you to come bring these questions to Formal Methods for the Informal Engineer ( https://fmie2021.github.io/ ), a workshop organized by myself and a few other researchers (including one or two more affiliated with LessWrong!) specifically dedicated to helping build collaborations to increase the adoption of formal methods technologies in the industry. Since it’s online this year, it might be a bit harder to have these deep open-ended conversations, but you sound exactly like the kind of person we want to attend. (To set expectations, I should add that registrations already exceed capacity; I’m not sure how we plan to allocate spots.)
I’d also like to share this list of formal methods in industry: https://github.com/ligurio/practical-fm . In the past decade, there’s been a huge (in relative, not absolute terms) increase in the commercial use of formerly Ivory Tower tools.
BTW, I’ve been trying to think about whom I know that directly works in language-based security. (defined as a narrow specialty). The main name that comes to mind that I personally know is Stephen Chong, but I think some of the Wyvern developers ( https://wyvernlang.github.io/ ) may also consider themselves in this category (and be easier to get ahold of than a Harvard professor).
I’m going to briefly hit some of your more narrow questions now. As an aside, be wary about saying “process” to a researcher—it’s used narrowly in ICSE circles to mean “methodology” (e.g.: Agile). I’m trying to mentally replace every use with “language-based security.”
the most security-promoting development processes that are currently in wide use.
I think Jim mostly gets it above: memory-safe languages and secure API design; also, implicitly, the type systems that make the latter possible.
In a way, this question is kinda self-answered by the framing, since language-based security primarily refers to language design, which primarily means type systems—this is in contrast to techniques such as static analysis, testing, model checking, symbolic execution, and sandboxing.
If you’re willing to be flexible about the “widely-used” statement, then individual companies have their own quirky languages, some of which have rather interesting restrictions. This language ostensibly used by OutSystems comes to mind ( https://link.springer.com/chapter/10.1007/978-3-642-19718-5_8 ), although I’m told by one of the authors that their actual implementation (as of 2013) is a bit simpler.
the most security-promoting development processes that are possible with recently developed technology
This is a tough question for me, because recent papers in this area tend to be about solving highly specific problems (the space of security problems is big, yo), and it takes a lot to generalize that to answer such a broad question. Also, I don’t follow latest developments that intensely. I’m going to take a pass.
processes that could come to exist 10 years away; processes that might exist 30-50 years from now.
Adam Chlipala thinks by that time we’ll be generating correct-by-construction code from specs. The Everest and Fiat-Crypto projects, both of which generate correct-by-construction cryptography code, are probably the two current best-known deployments of this.
perhaps some impossibility theorems that may bind even the creatures of the singularity.
“If it’s nontrivial to prove your program terminates, your program probably doesn’t run.”—an undergrad friend.
For common infrastructure software of today, no. Except maybe that I don’t know it’s been shown possible to build secure, reliable software atop a realistic model of hardware faults.
For Software 2.0 (i.e.: neural net in the loop), it’s a more open question that I don’t know much about.
For the kinds of reflective self-improvement software MIRI discusses, that’s part of their active research program (and generally outside the cognizance of PL/SE researchers).
but you sound exactly like the kind of person we want to attend
What, but I’m just a stray dog who makes video games about -… [remembers that I am making a game that centers around an esolang. Turns and looks at my BSc in formal languages and computability. Remembers all of the times a layperson has asked whether I know how to do Hacking and I answered “I’m not really interested in learning how to break things. I’m more interested in developing paradigms where things cannot be broken”]… oh.
Did not know about the answer/comment distinction! Thanks for pointing that out.
Before I dig deeper, I’d like to encourage you to come bring these questions to Formal Methods for the Informal Engineer ( https://fmie2021.github.io/ ), a workshop organized by myself and a few other researchers (including one or two more affiliated with LessWrong!) specifically dedicated to helping build collaborations to increase the adoption of formal methods technologies in the industry. Since it’s online this year, it might be a bit harder to have these deep open-ended conversations, but you sound exactly like the kind of person we want to attend. (To set expectations, I should add that registrations already exceed capacity; I’m not sure how we plan to allocate spots.)
I’d also like to share this list of formal methods in industry: https://github.com/ligurio/practical-fm . In the past decade, there’s been a huge (in relative, not absolute terms) increase in the commercial use of formerly Ivory Tower tools.
You may also be interested in the readings from this course: https://6826.csail.mit.edu/2020/
BTW, I’ve been trying to think about whom I know that directly works in language-based security. (defined as a narrow specialty). The main name that comes to mind that I personally know is Stephen Chong, but I think some of the Wyvern developers ( https://wyvernlang.github.io/ ) may also consider themselves in this category (and be easier to get ahold of than a Harvard professor).
I’m going to briefly hit some of your more narrow questions now. As an aside, be wary about saying “process” to a researcher—it’s used narrowly in ICSE circles to mean “methodology” (e.g.: Agile). I’m trying to mentally replace every use with “language-based security.”
I think Jim mostly gets it above: memory-safe languages and secure API design; also, implicitly, the type systems that make the latter possible.
There are a number of patterns in secure API design you might not know the names for, such as object capabilities ( https://en.wikipedia.org/wiki/Object-capability_model ).
In a way, this question is kinda self-answered by the framing, since language-based security primarily refers to language design, which primarily means type systems—this is in contrast to techniques such as static analysis, testing, model checking, symbolic execution, and sandboxing.
Leaving the realm of Turing-complete programs, I’ll point you to PNaCl/RockSalt ( https://news.harvard.edu/gazette/story/2012/07/nacl-to-give-way-to-rocksalt/ ) and eBPF, both of which have verified sandboxes.
If you’re willing to be flexible about the “widely-used” statement, then individual companies have their own quirky languages, some of which have rather interesting restrictions. This language ostensibly used by OutSystems comes to mind ( https://link.springer.com/chapter/10.1007/978-3-642-19718-5_8 ), although I’m told by one of the authors that their actual implementation (as of 2013) is a bit simpler.
This is a tough question for me, because recent papers in this area tend to be about solving highly specific problems (the space of security problems is big, yo), and it takes a lot to generalize that to answer such a broad question. Also, I don’t follow latest developments that intensely. I’m going to take a pass.
Adam Chlipala thinks by that time we’ll be generating correct-by-construction code from specs. The Everest and Fiat-Crypto projects, both of which generate correct-by-construction cryptography code, are probably the two current best-known deployments of this.
“If it’s nontrivial to prove your program terminates, your program probably doesn’t run.”—an undergrad friend.
For common infrastructure software of today, no. Except maybe that I don’t know it’s been shown possible to build secure, reliable software atop a realistic model of hardware faults.
For Software 2.0 (i.e.: neural net in the loop), it’s a more open question that I don’t know much about.
For the kinds of reflective self-improvement software MIRI discusses, that’s part of their active research program (and generally outside the cognizance of PL/SE researchers).
What, but I’m just a stray dog who makes video games about -… [remembers that I am making a game that centers around an esolang. Turns and looks at my BSc in formal languages and computability. Remembers all of the times a layperson has asked whether I know how to do Hacking and I answered “I’m not really interested in learning how to break things. I’m more interested in developing paradigms where things cannot be broken”]… oh.
uh. maybe.