Hacker News Reader

Comment by docandrew | Hacker News Reader

As powerful as fuzzing is, this is a good reminder why it’s not a substitute for formal verification in high-integrity or critical systems.

View on HN

.. or more pragmatically, safer languages where errors aren't exploitable to get remote code execution.

(I guess that semantics can also be seen as a formally verified property)

Given log4shell happened in one of the more aggressively sandboxed languages with mainstream adoption, the outlook isn't great.

Sandboxing is mostly irrelevant to the log4j error. You'd have to tell the sandbox to turn off reflection, which isn't really feasible in Java. And that's because Java is so poorly designed that big libraries are all designed to use reflection to present an API they consider usable.

Compare that to a language designed well enough that reflection isn't necessary for good APIs, for instance.

Dunno if I agree that libraries need reflection. Some do, but primarily in the dependency injection and testing space.

That's not really where you'd expect RCE-problems.

Yeah, I should say where developers don't think they need to use reflection.

Like, the log4j thing came from (among other design errors) choosing to use reflection to look up filters for processing data during logging. Why would log4j's developers possibly think reflection is an appropriate tool for making filters available? Because it's the easy option in Java. Because it's the easy option, people are already comfortable with it in other libraries. Because it's easy and comfortable, it's what gets done.

Some languages make reflection much more difficult (or nearly impossible) and other APIs much easier. It's far more difficult to make that class of error in languages like that.

> big libraries are all designed to use reflection to present an API they consider usable.

whistles in python

Python has first-class type objects. That's not the same thing as writing:

  pickle._getattribute(__import__(package), path)

everywhere, which is basically how Java reflection works half the time. In Python, you'd have something like copyreg.dispatch_table, and have plugin modules that register themselves in the table at load-time – limiting your attack surface to the modules you expect to be attack surface, rather than every single package accessible to the JVM.

Code executing in the JVM isn't sandboxed. Sandboxing could have indeed mitigated log4shell. Log4shell was a design where a too powerful embedded DSL was exposed to untrusted data in a daft way - the log("format here...", arg1, arg2) call would interpret DSL expressions in the args carrying logged data. One can even imagine it passing formal verification depending on the specification.

But more broadly the thing is that eliminating these low level language footguns would allow people to focus on the logic and design errors.

Upvote for log4shell. That's pretty funny.

Yes, a safer language is not enough, but it is a huge leap forward, so I'll take it.

That belongs to the 30% of exploits that we are left with, after removing the 70% others from C.

I think you are correct, but I do not think the average severity of these exploits is necessarily the same.

US agency for cyber security thinks otherwise.

>> US agency for cyber security thinks otherwise

NSA's Software Memory Safety recommendation:

https://media.defense.gov/2022/Nov/10/2003112742/-1/-1/1/CSI... (pdf)

I’d classify runtime reflection as an unsafe language feature, to be honest.

Actually, Elasticsearch was completely unaffected by log4shell precisely because they implemented JVM sandboxing which completely mitigated it: https://discuss.elastic.co/t/apache-log4j2-remote-code-execu...

Java Security Manager is deprecated in Java 17 and is likely to be removed in the future releases.

So better approach is to use container security or something like that.

The deprecation JEP has some discussion of why it was deprecated: https://openjdk.org/jeps/411

"The threat of accidental vulnerabilities in local code is almost impossible to address with the Security Manager. Many of the claims that the Security Manager is widely used to secure local code do not stand up to scrutiny; it is used far less in production than many people assume. There are many reasons for its lack of use: [...]"

Would be interesting to know if there were other cases besides ElasticSearch that were protected from log4j by JSM.

.NET also dropped CAS during the Core rewrite, with similar reasoning.

Which is a pity, but unfortunely capability based systems still seem to have a problem for the common developer to properly configure them.

Safer languages cannot protect from bad design. Many libraries have implicit behaviour which is not always visible. It's a hard tradeoff to make. You want safety, but in the same time enough customisation and features. I worked recently with an http client library which was forbidding to send special characters in headers. I understand that this is a safety feature, but I really wanted to send weird characters (building a fuzzing tool).

OK but we can mitigate these types of exploits (buffer overflow etc.) using memory-safe languages.

Bad design is a universal orthogonal problem.

That's true. It will definitely mitigate different category of exploits out of the box, but you still need people to acknowledge and be intentional about their decisions.

Seatbelts can not save you from bad driving, but they certainly help mitigate the effects.

Safer languages can protect from some kinds of bad design. Some kinds of incoherent design become simply impossible to express. (For example, using a structured language with function calls instead of goto means a function always returns to the same place where it was called from, so a whole class of possible designs - most of which were just mistakes, but a few of which were efficient implementations - becomes impossible)

One job of language designers and compiler writers is to recover the efficient implementations without allowing the bad designs.

See how eg optimized tail calls essentially give you back all the power of goto without the old downsides.

There's no replacement for intelligence. Turning the world into authoritarian dystopia in search of that replacement seems to be the popular thing to do, unfortunately.

I would argue the issue was not checking the coverage of new code vs what was being tested.

The OP is pointing out that what "the issue" is depends on whether you want high confidence that your code has few bugs, or you want certainty that your code contains no bugs.

> you want certainty that your code contains no bugs

Well, everyone would want that, but it's not possible. Formal verification comes nowhere close to promising that, especially not on a large project. I'm pretty sure OpenSSL is larger than any formally verified software to date (perhaps CompCert is larger?).

"Beware of bugs in the above code; I have only proved it correct, not tried it."

Donald Knuth

Reply on news.ycombinator.com