6 ms·

I really want to like this, but it really comes across as more of a wishful thinking project without a lot of experience or intuition about how to solve the ver

I really want to like this, but it really comes across as more of a wishful thinking project without a lot of experience or intuition about how to solve the very real problems that formal methods run into in this domain. Like, the design goals literally include "verify any program" [1], which is almost certainly impossible. Important questions like how you implement the design pillars without running smack into the issue of decidability seem entirely ignored. They have a whole section on how "this idea exists in an incentive no man's land" without seemingly being aware of the rich history of formal methods in low level programming, from Ada through Java through formal C through Rust itself. The common issues these encountered like decidability, holes in the formal model (which contributed to the downfall of the Java sandbox as a security boundary), and the combinatorial explosion inherent in verification tools are all huge looming questions that should at least be mentioned. Maybe I'm being overly critical here and partial improvements are still improvements, but it'd be nice to see more moderate claims from authors tackling such an ambitious project. [1] https://github.com/magmide/magmide/blob/main/posts/design-of-magmide.md https://github.com/magmide/magmide/blob/main/posts/design-of...

joek1301 4y ago
Could you elaborate / share resources on "downfall of the Java sandbox as a security boundary"? Sounds interesting.
- AlotOfReading 4y ago
  This all dates from the old days of Java 1.x and applets. The original idea was that the JVM could perfectly sandbox applications from hardware resources, so the smart people at Sun came up a very forward thinking architecture: Untrusted code could be cryptographically signed by a root of trust. Then, bytecode would be formally verified to prove the absence of certain kinds of bad behavior. Then JVM would take care of various low level details like memory management. Finally, for any high level behavior there was something called the Security Manager that allowed 'fine grained' permissions for so-called dangerous APIs. All of this was the sandbox. What happened in practice: * The bytecode verifier ended up being accidentally quadratic, leading to straightforward DoS attacks * The verifier kept having bugs, some of which stood for years * It was impossible to enforce resource usage policies like "don't use all of my CPU". Since cryptocurrency is now a thing, this problem has become somewhat more severe than it was 20 years ago. * The security model was useless in practice, because unverified or native code broke the entire thing. This remains an research open question under most conditions. * Oh god the bugs. They were endless and the practical result was that the sandbox was never secure. [1] recapped 20 years of exploits, if you're curious about examples. By the tail end of the system's life, even the public was completely fed up with it and mainstream media was publishing articles like [2]. Eventually even Oracle gave up and just deprecated both Applets and the SecurityManager system entirely [3]. [1] http://phrack.org/issues/70/7.html#article http://phrack.org/issues/70/7.html#article [2] https://www.reuters.com/article/oracle-security/oracle-fixes-42-holes-in-java-to-revive-security-confidence-idUKL2N0D32C620130416 https://www.reuters.com/article/oracle-security/oracle-fixes... [3] https://openjdk.java.net/jeps/411 https://openjdk.java.net/jeps/411
- IncRnd 4y ago
  Not the GP, but the Java Sandbox is now deprecated. There is an already closed deprecation ticket at openjdk.java.net.[1] For a blog post at inside.java see here.[2] Both links have some explanatory information. [1] https://openjdk.java.net/jeps/411 https://openjdk.java.net/jeps/411 [2] https://inside.java/2021/04/23/security-and-sandboxing-post-securitymanager/ https://inside.java/2021/04/23/security-and-sandboxing-post-...
johnbender 4y ago
To follow on this sentiment at a slight tangent, I am happy for the enthusiastic attempts from all quarters but folks seem to misunderstand that incremental progress in academia is often due to the problems being very hard. Formal verification in the presence of weak memory models is an ongoing problem that only recently has seemed tractable thanks to the hard work of the folks at MPI etc over more than a decade of publications and iterating on logics like Iris
agentultra 4y ago
It is wishful thinking. Iris is cool and all but extracting useful programs from proofs is still an open research area. I don’t want to discourage someone from trying but it would help to be pragmatic. At least the author seems somewhat aware of this when they describe the repo as a collection of earnings and ravings. I’ve been interested in this since 2015 or so and even then the cost of doing formal verification had come down a lot. It has continued the downward trend. But we are still a long way from a language that industry programmers can use to write proofs and extract programs from. One of the major challenges will be teaching industry programmers how to write proofs and convincing them that they want to do this.
- petergeoghegan 4y ago
  > One of the major challenges will be teaching industry programmers how to write proofs and convincing them that they want to do this. "Industry programmers" are pretty far from being a monolith. There are a myriad of different approaches to testing, many of which are domain specific, for all kinds of reasons. Usually the way that a new testing tool gets adapted is that individual programmers or companies that adapt the tool appear to have a competitive advantage over those that don't. The results generally speak for themselves, at least after a time. Practically everybody that might use formal verification has already chosen to not go to certain lengths to increase reliability. They're already making an economic trade-off -- even with safety critical systems, or in domains where the cost of bugs is extraordinarily high. Why shouldn't formal verification be assessed in the same way?
  - Hizonner 4y ago
    Because many of the costs of their irresponsible practices are externalized.
    - petergeoghegan 4y ago
      > Because many of the costs of their irresponsible practices are externalized. I'm sure that that's true in at least some important cases. I don't see what it has to do with formal verification.
Hizonner 4y ago
I agree it sounds like pretty naive enthusiasm. Not just about how hard the formal verification problem is, but about how hard it is to get ANY kind of programming system up to the point where it's actually usable. However, every time somebody starts going negative on formal verification by talking about decidability, I get itchy. Sure, we know, all interesting properties of programs in all interesting languages are undecidable in general. Rice's theorem, blah, blah, blah. For any given property and any given language, I can show you a program in that language such that you cannot determine whether that program has that property. ... but it turns out that most actually INTERESTING PROGRAMS aren't like that. When you really write code to get something done, you you generally have a reason to believe that code is going to work. That means that the code is least approximately correct by construction, and correct in a way that's comprehensible and locatable. Often the machine will be able to find a proof that it's correct. If not, you'll often be able to provide hints. And if neither you nor your computer can find a proof, that probably means you don't understand the code enough to want to use it to begin with. Oh, and on computational cost of verification, you can get some relief by passing around precomputed proofs along with the source code, so they only have to be checked on installation, or incrementally recomputed when the code is modified, rather than being rebuilt from scratch every time.
- _vdpp 4y ago
  A lot of people take undecidability to mean “no program can be proven to terminate” when in reality it means “there exist programs which are impossible to prove termination,” and like you said most of the useful programs we write can be shown to terminate just fine.
  - kaba0 4y ago
    You forget about Rice’s theorem. Termination is not that exciting, but the existence of race conditions and a million other properties are - and those are not possible to prove true in general.
    - ebingdom 4y ago
      No, docandrew is correct. You are incorrectly applying Rice's theorem. Rice's theorem states that those properties can't be automatically decided in general. But that's irrelevant to this discussion, because this "magmide" tool doesn't claim to do that. It merely checks proofs that have already been found (e.g., by a human), which is trivially decidable.
drc500free 4y ago
It gives me the same feeling as crypto-contracts. Someone with a very narrow range of low-level experience arm-chairs their way into a solution for a problem. That problem isn't even the hard problem for the domain, but they've thought a lot about it in a vacuum. What is the "verifiability" of an e-commerce funnel? Of a recommendation engine? Of a national identity card system? It doesn't take a lot of real-world experience to recognize that the specification process is generally more error-prone and imprecise than the coding process, but it does take some.

joek1301 4y ago

Could you elaborate / share resources on "downfall of the Java sandbox as a security boundary"? Sounds interesting.

AlotOfReading 4y ago
This all dates from the old days of Java 1.x and applets. The original idea was that the JVM could perfectly sandbox applications from hardware resources, so the smart people at Sun came up a very forward thinking architecture: Untrusted code could be cryptographically signed by a root of trust. Then, bytecode would be formally verified to prove the absence of certain kinds of bad behavior. Then JVM would take care of various low level details like memory management. Finally, for any high level behavior there was something called the Security Manager that allowed 'fine grained' permissions for so-called dangerous APIs. All of this was the sandbox. What happened in practice: * The bytecode verifier ended up being accidentally quadratic, leading to straightforward DoS attacks * The verifier kept having bugs, some of which stood for years * It was impossible to enforce resource usage policies like "don't use all of my CPU". Since cryptocurrency is now a thing, this problem has become somewhat more severe than it was 20 years ago. * The security model was useless in practice, because unverified or native code broke the entire thing. This remains an research open question under most conditions. * Oh god the bugs. They were endless and the practical result was that the sandbox was never secure. [1] recapped 20 years of exploits, if you're curious about examples. By the tail end of the system's life, even the public was completely fed up with it and mainstream media was publishing articles like [2]. Eventually even Oracle gave up and just deprecated both Applets and the SecurityManager system entirely [3]. [1] http://phrack.org/issues/70/7.html#article http://phrack.org/issues/70/7.html#article [2] https://www.reuters.com/article/oracle-security/oracle-fixes-42-holes-in-java-to-revive-security-confidence-idUKL2N0D32C620130416 https://www.reuters.com/article/oracle-security/oracle-fixes... [3] https://openjdk.java.net/jeps/411 https://openjdk.java.net/jeps/411
IncRnd 4y ago
Not the GP, but the Java Sandbox is now deprecated. There is an already closed deprecation ticket at openjdk.java.net.[1] For a blog post at inside.java see here.[2] Both links have some explanatory information. [1] https://openjdk.java.net/jeps/411 https://openjdk.java.net/jeps/411 [2] https://inside.java/2021/04/23/security-and-sandboxing-post-securitymanager/ https://inside.java/2021/04/23/security-and-sandboxing-post-...

johnbender 4y ago

To follow on this sentiment at a slight tangent, I am happy for the enthusiastic attempts from all quarters but folks seem to misunderstand that incremental progress in academia is often due to the problems being very hard. Formal verification in the presence of weak memory models is an ongoing problem that only recently has seemed tractable thanks to the hard work of the folks at MPI etc over more than a decade of publications and iterating on logics like Iris

agentultra 4y ago

It is wishful thinking. Iris is cool and all but extracting useful programs from proofs is still an open research area. I don’t want to discourage someone from trying but it would help to be pragmatic. At least the author seems somewhat aware of this when they describe the repo as a collection of earnings and ravings. I’ve been interested in this since 2015 or so and even then the cost of doing formal verification had come down a lot. It has continued the downward trend. But we are still a long way from a language that industry programmers can use to write proofs and extract programs from. One of the major challenges will be teaching industry programmers how to write proofs and convincing them that they want to do this.

petergeoghegan 4y ago
> One of the major challenges will be teaching industry programmers how to write proofs and convincing them that they want to do this. "Industry programmers" are pretty far from being a monolith. There are a myriad of different approaches to testing, many of which are domain specific, for all kinds of reasons. Usually the way that a new testing tool gets adapted is that individual programmers or companies that adapt the tool appear to have a competitive advantage over those that don't. The results generally speak for themselves, at least after a time. Practically everybody that might use formal verification has already chosen to not go to certain lengths to increase reliability. They're already making an economic trade-off -- even with safety critical systems, or in domains where the cost of bugs is extraordinarily high. Why shouldn't formal verification be assessed in the same way?
- Hizonner 4y ago
  Because many of the costs of their irresponsible practices are externalized.
  - petergeoghegan 4y ago
    > Because many of the costs of their irresponsible practices are externalized. I'm sure that that's true in at least some important cases. I don't see what it has to do with formal verification.

Hizonner 4y ago

I agree it sounds like pretty naive enthusiasm. Not just about how hard the formal verification problem is, but about how hard it is to get ANY kind of programming system up to the point where it's actually usable. However, every time somebody starts going negative on formal verification by talking about decidability, I get itchy. Sure, we know, all interesting properties of programs in all interesting languages are undecidable in general. Rice's theorem, blah, blah, blah. For any given property and any given language, I can show you a program in that language such that you cannot determine whether that program has that property. ... but it turns out that most actually INTERESTING PROGRAMS aren't like that. When you really write code to get something done, you you generally have a reason to believe that code is going to work. That means that the code is least approximately correct by construction, and correct in a way that's comprehensible and locatable. Often the machine will be able to find a proof that it's correct. If not, you'll often be able to provide hints. And if neither you nor your computer can find a proof, that probably means you don't understand the code enough to want to use it to begin with. Oh, and on computational cost of verification, you can get some relief by passing around precomputed proofs along with the source code, so they only have to be checked on installation, or incrementally recomputed when the code is modified, rather than being rebuilt from scratch every time.

_vdpp 4y ago
A lot of people take undecidability to mean “no program can be proven to terminate” when in reality it means “there exist programs which are impossible to prove termination,” and like you said most of the useful programs we write can be shown to terminate just fine.
- kaba0 4y ago
  You forget about Rice’s theorem. Termination is not that exciting, but the existence of race conditions and a million other properties are - and those are not possible to prove true in general.
  - ebingdom 4y ago
    No, docandrew is correct. You are incorrectly applying Rice's theorem. Rice's theorem states that those properties can't be automatically decided in general. But that's irrelevant to this discussion, because this "magmide" tool doesn't claim to do that. It merely checks proofs that have already been found (e.g., by a human), which is trivially decidable.

drc500free 4y ago

It gives me the same feeling as crypto-contracts. Someone with a very narrow range of low-level experience arm-chairs their way into a solution for a problem. That problem isn't even the hard problem for the domain, but they've thought a lot about it in a vacuum. What is the "verifiability" of an e-commerce funnel? Of a recommendation engine? Of a national identity card system? It doesn't take a lot of real-world experience to recognize that the specification process is generally more error-prone and imprecise than the coding process, but it does take some.