IRC channel logs
2023-04-28.log
back to list of logs
<oriansj>gforce_de1977: so no prebuilt ppc32 linux distro isos available? <oriansj>fitzsim: yeah, the more information provided on how to get to a functional ppc64be qemu setup would be very helpful in getting a ppc64be port <stikonas>oriansj: can't you just use qemu user emulation? <stikonas>I can see it has support for both ppc64 and ppc64le <stikonas>well, there might be an ocassional small bug with user emulation (e.g. registers not zeroed...) <stikonas>but arguably we should initialize everything we use <oriansj>stikonas: in theory yes but I am not going to do that. There are a good few reasons why if I can't build a qemu Linux system for an architecture not to bother doing the work needing to port an architecture. <oriansj>I might make an exception for netbsd if that was better supported in M2libc but I will not support non-free operating systems. <fossy>ppc32 is a bit of an odd architecture... <fossy>ppc64le is the most common by far, ppc32 is really only power macs <fossy>i don't blame them, there's no hardware for it! <fossy>(no hardware made in the last 15 years, at least :P) <fossy>figured out the problem with gh actions - nongnu does not like depth=1 cloning when you are not cloning HEAD <FlaminWalrus>Hey y'all, I saw the Guix blog post about the project, and I had a few questions about the "trusting trust" side of the story. My ultimate, extreme-distant-future hope for its resolution is a complete reduction of all software trust to (meta)physical and epistemological axioms. The final solution I envision is roughly a printed list of natural-language instructions that a determined someone could follow, and, after a decent amount <FlaminWalrus>sweat, obtain a trustworthy modern software stack to be used for other verification purposes (say, checking Lean mathlib, verifying correctness of the seL4 kernel, or mining BTC). How hard of trust dependencies are a POSIX kernel and Guile/kaem trust dependencies? Also, are there plans or hopes to use formal methods to provide natural-language specifications and correctness proofs of the various stages? Are the near-term steps mor <FlaminWalrus>focused around architecture ports or kernel/shell binary reduction? <stikonas>kaem-optional-seed is tiny enough that you can inspect it manually <stikonas>builder-hex0 is now about 4 KiB of hex0 code but perhaps we'll have a smaller hex0 seed and what is currently builder-hex0 will be built from hex2 code, so in terms of software you could check everything <stikonas>not sure about natural language specifications, we don't really have that <stikonas>as for more architecture ports, we have quite a few architectures in stage0-posix (more could be added) but so far very few are supported in stage0-posix to mes step and even fewer in mes/meccc to tcc-0.9.26 <janneke>if you run: "guix install --no-substitutes hello", then the whole bootstrap will be run for you <janneke>not sure how much more natural language instructions you'd want? <stikonas>it's mostly run this command, then that command, etc ... <FlaminWalrus>janneke: Well, there's a trust dependency on the entire system in which you run that command <stikonas>the whole thing can be driven by kaem-optional-seed <stikonas>and almost everything (small part is missing) can be driven if you start with builder-hex0 kernel <FlaminWalrus>stikonas: does the kaem-optional-seed bootstrap depend on a kernel? Do you know where I can find binary sizes for these? <stikonas>FlaminWalrus: yes, and no... there is more than one kaem-optional-seed <janneke>fwiw, i'm working on a system with builtin formal verification, but i fail to see how something like that would apply here -- maybe if someone would want to write a kernel <stikonas>FlaminWalrus: so if you dont want to run on guix, there is live-bootstrap project that can run on either Linux inside chroot/namespaces. Or it can run on QEMU baremetal with some kernel, you can use Linux or you can start with builder-hex0 (4 KiB) <stikonas>if you start with builder-hex0 kernel, then the whole process runs up to the point where Linux kernel is built <stikonas>but we have not implemented kexec'ing into Linux kernel yet <stikonas>FlaminWalrus: there is also stage0-uefi where no kernel is used, but that stops after you reach the end of stage0 as we haven't ported mes to UEFI <stikonas>but you could use stage0-uefi to build some POSIX binaries <stikonas>hex0 is 256 bytes, but both depend on kernel <FlaminWalrus>jannecke: it would apply because specifications is the name we give sufficiently good documentation---a full-source bootstrap is only as good as your guarantees that the code is correct, so for, say, removing dependence of seL4's formal correctness proofs on whatever's used to compile the Isabelle trusted kernel, you need correctness proofs of everything you bootstrap up until that point <stikonas>FlaminWalrus: though the size is not everything. UEFI seeds have much bigger PE32 headers compared to ELF headers on Linux, but PE32 header has lots of zeroes in it <stikonas>FlaminWalrus: but correctness proof in what ? <FlaminWalrus>As with most metalogic, you would use natural-language mathematical reasoning <FlaminWalrus>Such proofs would be the highest standard of an audit record it would be useful to achieve, I think <stikonas>well, you will have to start with the correctness of hex0 <FlaminWalrus>Silicon vendors publish (at least semi-) formal specifications of the ISA <FlaminWalrus>The seL4 kernel, for instance, proves correctness of the entire binary against a well-defined-C-subset source via SAT-solving <stikonas>yes, but you can't use seL4 kernel for this <FlaminWalrus>If you have smaller binaries, the specifications and witness truth-assignments are smaller <stikonas>you have to do actual mathematical proof with pen and paper <stikonas>and then that still depends on silicon being correct <stikonas>but that's hardware trusting trust problem... <FlaminWalrus>I can mentally sketch a process for removing dependence on flashing software/hardware, and think that's probably atainable (maybe using some ancient disk tech and a switch-coded vacuum tube monstrosity) <FlaminWalrus>But I have no idea how to begin tackling verifying particular silicon's correctness against the ISA spec, even probabilistically, much less all the supporting hardware <FlaminWalrus>Baby steps, though; if we can get software that's a huge accomplishment <FlaminWalrus>In summary of the current-status talk, though: the shell part is reasonably auditable with keam, and there are lots of different ways to attack the kernel problem <stikonas>yeah, we don't use many syscalls early in the bootstrap <stikonas>(which is one of the reasons why we can have some small POSIX kernels that can run stage0-posix) <stikonas>it's a bit bigger, probably at the limits of what you can expect to audit <stikonas>but like I said later we can try to switch to something smaller <stikonas>hex0 is quite hard to work with, because any edit might cause all the relative jumps in the code to change <stikonas>and starting form hex1 and hex2 things are much easier <FlaminWalrus>So, I'm gathering the current process is completely kernel-independent before hex2? Is it also shell-independent? <stikonas>we need kernel, but we might be able to produce a smaller one <stikonas>there is already builder-hex0-mini but it would need some changes <stikonas>at the moment builder-hex0 supports all the way to running tcc <stikonas>and this is quite a bit more than what we need to run hex2 <stikonas>FlaminWalrus: but UEFI binaries are kernel independent <stikonas>we can build e.g. M2-Planet.efi that runs without any kernel and can self-host <stikonas>but also header is much bigger (nut not much more complicated, it largely consists of zeroes) <FlaminWalrus>(Sorry for the questions that may seem somewhat repetitive---still trying to learn the ecosystem) <stikonas>later UEFI binaries are also a bit bigger <stikonas>that's the only thing you have on most modern hardware <FlaminWalrus>There actually have been (at least proof-of-concept) attacks via UEFI bugs, IIRC <stikonas>but if alternative on most hardware is UEFI + kernel + something <FlaminWalrus>Yep, I think it's safe to consider UEFI part of the "hardware" problem <stikonas>anyway, it's just one of the options that we created <stikonas>and some UEFIs are small enough (e.g. U-Boot) <stikonas>anyway, early steps hex0, hex1, hex2 mostly need just input and output <FlaminWalrus>Is there anywhere where there's a unified list of up-to-date project components? I think I stumbled through several archived/outdated READMEs on my way here <stikonas>UEFI bugs are probably mostly related to Secure boot, aren't they <stikonas>also depends what do you mean by components? <FlaminWalrus>Noted. Thanks for your time; I've got to run for the moment but will be back later today, likely with more questions. <stikonas>but we don't have a very good description of all projects that we have <oriansj>we do have the previous talks and talk notes but ultimately the best way to learn is to talk to other humans.