3 ms·

I'm just taking two lines from the article: "Reliability and proven tools are even more important than libraries"... in this case, there are a lot of proven too

I'm just taking two lines from the article: "Reliability and proven tools are even more important than libraries"... in this case, there are a lot of proven tools for writing C programs, including the theorem provers. And "You're more dependent on the decisions made by the language implementers than you think"... there have been a lot of flaws in the JRE over time, most of them from the parts of the JRE that are written in C. If you had been writing in C, you could have avoided those flaws if you were in the top 2% most diligent and careful C programmers, because the C tools are rock solid, whereas Java tools haven't been (January 2013 is still pretty recent). Problems in libraries, such as heartbleed, can be mitigated in C using the same tools that you'd use in Java. Process isolation is great. Of course, if you are writing your web app in C then I am going to replace you with someone else. But the web is not everything.

heinrich5991 12y ago
What is such a theorem prover? I'm interested in it for trying to prove properties of my own programs...
lmm 12y ago
The January 2013 flaws affected end users running the browser plugin, not systems written in Java. I suppose if you had a system that allowed users to submit their own bytecode and used Java's native facilities for handling this, then you'd be vulnerable. But nothing forces you to do that; someone who's capable of writing a safe bytecode verifier in C is certainly capable of writing one in Java. The only even vaguely recent flaw I can remember in the JRE was, as you say, in the part written in C (I think in some image loading code). It takes a very perverse kind of logic to say: this system which is mostly not-C and a tiny bit C keeps having security flaws in the C part, therefore we should switch to systems which are written more in C. If the tooling for verifying C is really so good, why not verify the C parts of the JRE? Then they'd be proven once and for all, and lots of systems would benefit.
- dietrichepp 12y ago
  > If the tooling for verifying C is really so good, why not verify the C parts of the JRE? Then they'd be proven once and for all, and lots of systems would benefit. I'm going to quote the article again... > You're more dependent on the decisions made by the language implementers than you think. When you use Java, you don't have the opportunity to second-guess the choices that produced the JRE. And I think you're not quite getting what I'm saying: I'm not saying that "we should switch to systems which are written more in C", I'm saying that writing systems in C protects you from mistakes in the JRE (which you have no control over) in exchange for exposing you to your own mistakes (which you can control). You can then spend a large amount of time and money developing and verifying your system. The goals and constraints of your project will determine whether this is a good trade-off. I'm certain that Java is preferable for writing the vast majority of web apps, but the web is not everything. > If the tooling for verifying C is really so good, why not verify the C parts of the JRE? First, I'm going to guess that an enormous amount of static and dynamic analysis has been done on the JRE. Bugs in it are rather rare these days, given its size and complexity. However, verification tools are generally not suited to this particular task. Verification tools are better at verifying typical application code, and the JRE needs to do a lot of very unusual operations in order to work. In cases where you'd use verification, you'd also typically use a "safe" subset of C. Some of these subsets don't even permit dynamic memory allocation, or if so, only permit it at program startup. So, it may actually be more straightforward to deliver a working Mars rover in C than it would be to deliver a verified JRE. Neither task is easy.

heinrich5991 12y ago

What is such a theorem prover? I'm interested in it for trying to prove properties of my own programs...

lmm 12y ago

The January 2013 flaws affected end users running the browser plugin, not systems written in Java. I suppose if you had a system that allowed users to submit their own bytecode and used Java's native facilities for handling this, then you'd be vulnerable. But nothing forces you to do that; someone who's capable of writing a safe bytecode verifier in C is certainly capable of writing one in Java. The only even vaguely recent flaw I can remember in the JRE was, as you say, in the part written in C (I think in some image loading code). It takes a very perverse kind of logic to say: this system which is mostly not-C and a tiny bit C keeps having security flaws in the C part, therefore we should switch to systems which are written more in C. If the tooling for verifying C is really so good, why not verify the C parts of the JRE? Then they'd be proven once and for all, and lots of systems would benefit.

dietrichepp 12y ago
> If the tooling for verifying C is really so good, why not verify the C parts of the JRE? Then they'd be proven once and for all, and lots of systems would benefit. I'm going to quote the article again... > You're more dependent on the decisions made by the language implementers than you think. When you use Java, you don't have the opportunity to second-guess the choices that produced the JRE. And I think you're not quite getting what I'm saying: I'm not saying that "we should switch to systems which are written more in C", I'm saying that writing systems in C protects you from mistakes in the JRE (which you have no control over) in exchange for exposing you to your own mistakes (which you can control). You can then spend a large amount of time and money developing and verifying your system. The goals and constraints of your project will determine whether this is a good trade-off. I'm certain that Java is preferable for writing the vast majority of web apps, but the web is not everything. > If the tooling for verifying C is really so good, why not verify the C parts of the JRE? First, I'm going to guess that an enormous amount of static and dynamic analysis has been done on the JRE. Bugs in it are rather rare these days, given its size and complexity. However, verification tools are generally not suited to this particular task. Verification tools are better at verifying typical application code, and the JRE needs to do a lot of very unusual operations in order to work. In cases where you'd use verification, you'd also typically use a "safe" subset of C. Some of these subsets don't even permit dynamic memory allocation, or if so, only permit it at program startup. So, it may actually be more straightforward to deliver a working Mars rover in C than it would be to deliver a verified JRE. Neither task is easy.