Follow

The recent exploit around Bluetooth in the Linux Kernel is caused by type insecurity, unsurprisingly. Perhaps it is time to reevaluate the merits of writing system internals in type safe languages like OCaml which have high performance, memory safety, type safety, and thread safety. Or at least start working in static analyzers, like Frama-C to fuzz out this shit.

@brettgilio OCaml isn't really suitable for writing OS kernels, it's very automatic and it's runtime is pretty huge: you need to operate on the memory very precisely, keeping an eye on the exact sizes of the values and caching issues, the ISRs (interrupt handlers) have to be very small and accurate, and, for embedded applications, the output binary should be small overall.

Also OCaml lacks linear types (lacked, last time I checked).

Mirage OS is written in OCaml, but it doesn't contain as many device drivers...

Frama-C is interesting, but you have to write specifications by hand, and that's not a trivial task. Also you may need to guide the provers in some (a lot of actually) cases.

I'd rather consider Ada/SPARK as the language for "device-oriented" programming.

@brettgilio Meanwhile. OCaml is just fine in places where Python is mostly used these days: back-end of Web-applications, scripting for special-purpose s/w (data analysis, computer-aided design, etc.).
For the former, you can run the application right on top of a hypervisor (KVM), without the need for a kernel (Linux) and base system (Glibc etc.). Thanks to Mirage.

@brettgilio Sure you still need a hypervisor. But I'm not sure it has to be implemented in software at all...

@amiloradovsky @brettgilio Ada doesn't have nearly enough advocacy so many people haven't seen what it really looks like.
That was one of my goals for writing github.com/dmbaturin/hvinfo (other than saving the world from a mess of C and shell that most other tools like virt-what are).

@lthms @amiloradovsky @brettgilio Looks interesting for sure.
There's also a verified type1 hypervisor in Ada: muen.sk/

@doktorkrek Yes. Have you heard about how Rust's promises of safety are meaningless because it lacks a spec, a standard unified ABI, and avoids the type system constantly?

Sign in to participate in the conversation
Mastodon 🐘

Discover & explore Mastodon with no ads and no surveillance. Publish anything you want on Mastodon: links, pictures, text, audio & video.