Integrating “safe” languages into OpenBSD?

I have spent a long time using alternative languages. I'm a compiler geek. However, most of these languages ultimately lead to disappointment. Not because they necessarily fail, but rather because the problem of writing software is not a problem of language or platform. It is a problem of thought and abstraction. So, the big promises that these new languages and platforms make will ultimately only be fulfilled for a subset of applications. The rest of the time, we must still trudge through the process of good design, good testing, and good real-world feedback.

People love to beat up on C, because it does not have feature X or feature Y, and because there is plenty of bad C software to point at. However, it isn't the language that leads to bad software. Any entrenched popular language has plenty of bad software examples, and plenty of security vulnerabilities. The problem isn't the language, but rather, the developer. A good developer who understands and appreciates the problem can write good software in machine code, C, C++, Rust, Java, Haskell, C#, Go, D, or any other language or platform. A good developer who understands secure programming processes can write secure software in any of these languages, given enough time.

What these higher-level languages offer is better abstraction, which can make time-to-market faster. However, in a deeply entrenched system that is already in market, maintaining the current languages and platforms is typically the better play. This is especially true when the source code is as meticulously maintained as it is with OpenBSD. Someone who understands the basics of C can easily read the OpenBSD kernel or userland, and understand everything about how a given program works. Some knowledge of BSD Make, Bourne shell, Korn shell, and Perl may be required to understand the init scripts and build process, but in all, it is a system that is easy to understand, easy to maintain, and with an excellent development process in place to deliver two builds a year. OpenBSD isn't broke, and a new language isn't going to fix it.

That being said, there are tools that the OpenBSD team could use that neither impact the build time nor require adopting fad language of the week. There are excellent model checkers out there for C, and quite a few proof assistants are gaining the ability to check proofs on C code directly, using Separation Logic and Hoare triplets. These tools can complement an entrenched C system by providing an external mechanism of verification that allows designers to formally verify that implementation meets specification. While formally verifying all of OpenBSD would be a tall order, taking hundreds of man years, formally verifying critical pieces of the kernel and creating simplified contract boundaries for the remaining code would be an excellent complement to the code review process that the OpenBSD team already does. Better still, it is something that could pay off without reinventing OpenBSD to match the current fad, as such verification can be run independently of the standard build process. If I were to make a suggestion to the OpenBSD team, it would be to explore such tools. But, to de Raadt's point, such a suggestion would only be valid if someone did the heavy lifting to put such a tool in place, and if it were of utility to the team. They won't adopt something for the sake of that thing, but they are keen for anything that can practically improve the security of their system.

> People have told me for the longest time that Java is a shitty language I shouldn't be using.

Java is a great language in theory, the problem with Java is that people have evolved to use layers upon layers upon even more layers of abstractions, the tooling is horrenduos (try configuring maven vs npm) and especially all complex Java applications end up being as slow as molasses (e.g. SAP GUI, Lotus Notes, Eclipse, jDownloader, Vuze on the GUI application side).

This leads to people projecting their horrible experiences with the Java ecosystem and applications to the language itself, which is a pity.

It's not undefeatable. The guy who invented it in 1970's, Paul Karger, told people the concepts on how to defeat it right afterward. Their advice for building systems in a way to catch a lot of subversion was encoded in the first standards for information security. I included most of those methods in my security framework here:

https://pastebin.com/y3PufJ0V

https://en.wikipedia.org/wiki/Trusted_Computer_System_Evalua...

One compiler made to the highest standard in development assurance is CompCert.

http://compcert.inria.fr/

It has specs of everything it does, proofs it does it in tool with minimalist checker, extracts to ML that can be compared against those specs in various ways (eg visually), can optionally be compiled with a mini-ML compiler or Scheme you homebrew yourself, and passed exhaustive testing by third party with only a few bugs in specs (not code). There's another using formal specs called KCC which could be ported to something bootstrappable like META II or Scheme.

The other requirement from TCSEC was that source be supplied to customer to build with their onsite, trusted tools. I looked into even having compilers done in Perl since it's already widely deployed. David A. Wheeler made brilliant suggestion of either bash or awk. I have put tools for those and more on rain1's bootstrapping page. rain1 or someone there called the concept "Ubiquitous Implementations." Note we've focused on technical content, not presentation, on that one being busy folks. Looks rough. :)

http://bootstrapping.miraheze.org/

You also need repo security to protect that source with it either cryptographically sealed and/or sent over secure transport. Link below on repo security from David A. Wheeler. Quite a few forms of transport security now.

https://www.dwheeler.com/essays/scm-security.html

After Thompson wrote on Karger's attack in 1980's, it took a life of its own among people that continue to mostly ignore the prior solutions. It's a problem absolutely solved to death starting with the person who discovered it in MULTICS Security Evaluation. Far as state-of-the-art, the current path of research is exploring how to integrate solutions for many languages, models, or levels of detail in one picture of a system with no abstraction gap attacks with proof of that for all inputs. That's a bit more complex but just an imperative language to assembly delivered and bootstrapped? Straight-forward but tedious, time-consuming work the first time it's done. :) Also, expensive if you buy CompCert which is only free for GPL stuff. Two of us are eyeballed CakeML's lowest-level languages as a cheat around that for verified bootstrapping.

http://cakeml.org/

EDIT: Btw, all that is technical discussion and argument. For fun, you might enjoy the story "Coding Machines" which is about only coding-related story I started reading and couldn't put down. Probably took an hour to read. It covers discovery of a Karger-Thompson-style attack along with how people might respond mentally and in terms of solutions. Some other stuff in that one.

http://www.teamten.com/lawrence/writings/coding-machines/

Thank you for saving me the trouble of writing that.

...And the point is that the OpenBSD project has a policy of self-hosting. The bootstrap compiler for base (along with everything else needed to build base) must exist in base.