[tptacek]

Your "first solution" would be to take a de novo PDF implementation written in C, "compile it with something that makes it memory-safe", and then port it to an L4 microkernel. Maybe bust out some HDL and get parts of it deployed directly on to FPGA.

Got it.

[nickpsecurity]

I said a separation kernel like the FOSS projects and commercial products dating back to 2005 I told Joanna about on Qubes mailing list which were compartmentalizing things on security-focused kernels. Aside from small TCB, they have optional mitifations for storage and timing channels. Aside from isolation, a standard practice on embedded side was including safe subsets of Java or Ada running right on the kernel to implement specific components more safely. So, basically just what was standard, deployed practice in high security over a decade ago.

Optionally, I also pointed out people interested in developing solutions have options available now for safety or security on CPU side, too. They can do software, hardware, mix of both, whatever suits their purposes.

[tptacek]

Oh, and a safe subset of Java or Ada in the kernel. Well, that clears it all up.

[nickpsecurity]

"safe subsets of Java or Ada running right on the kernel to implement specific components more safely. "

"a safe subset of Java or Ada in the kernel."

Done here since you're arguing against points Im not making. For anyone your strawman confused, the specific components are user-mode apps running on a separation kernel to minimize privilege. Not just piles of extra code in some kernel.