IRC channel logs
2023-04-29.log
back to list of logs
<roconnor>It's taking me 3 times around tcc and musl ofr musl's libc to reach a fixed point. <fossy>janneke: builtin formal verification sounds very interesting! what does that entail <fossy>FlaminWalrus: IMO, the biggest software dependency we don't really have a solution to is writing to a storage medium to read the bootstrap from <fossy>and the distribution of the material required for the bootstrap <fossy>putting the bootstrap onto a storage medium obviously requires software - and i don't have a clue how to remove that <janneke>fossy: a simple component-based programming language that separates control from data (and not looking at data for now), https://dezyne.org <janneke>components and their interfaces are translated into mCRL2 code (https://mcrl2.org) to produce LTSs to prove a number of characteristics <FlaminWalrus>fossy: I feel like dedicated, application-specific auditable hardware is the only solution for this---say, a disk that exposes a UART as well as a SATA interface, and an electromechanical keyboard or an 8-bit microscope-auditable, switch-programmed microcontroller that writes the boot code via the UART <FlaminWalrus>Which means it borders on the whole hardware can of worms I'm content to put off until we figure out the software side <Christoph[m]>Would it be possible to prove correctness of hardware with software tests? Or is that impossible because a system cannot prove its own correctness? <stikonas[m]>well, to strictly "prove" I guess it's impossible. But in practice that's what hardware developers do <stikonas[m]>(and also software developers when testing software) <stikonas[m]>it gives you some confidence that things are working <stikonas[m]>you can't detect hardware gaming your software tests... <muurkha>yeah, it's impossible to get reasonable confidence that there isn't a malicious backdoor <muurkha>we might be able to solve that with homeomorphic encryption <muurkha>where the potentially backdoored hardware can't tell what it's running <muurkha>encryption can also, more practically, help a lot with the storage-medium problem <muurkha>I mean we're already doing that by checking hashes <muurkha>but if you encrypt everything that goes to the storage medium with authenticated encryption using a key the attacker doesn't know, the storage medium can't subvert the bootstrap <muurkha>in software, formal proofs *can* give you reasonable confidence there isn't a malicious backdoor, but not in hardware <river>I am not sure if that approach will help <oriansj>FlaminWalrus: well if one has a trusted boot rom, it wouldn't take much to have a simple program that reads from some interface and just dumps it onto some disk. probably just a few hundred bytes. <river>it may be better to try to build safe hardware frmo scratch <river>or maybe run the same thing on a variety of hardware. this would demand bytecode vms rather than native code though. maybe not an option <oriansj>Nexus Intruder Class compromised hardware is just a harder problem in general <oriansj>(hardware that subverts software, to ensure next generation of hardware is subverted too) <river>software may be able to identify errors in hardware, but it cannot prove a lack of errors <stikonas_>exactly, software is in lower privilege level if you think of privilege rings <probie>Is it currently possible to go from Hex0 to a modern gcc on arm64, or are there some steps missing? <stikonas>we have very early steps hex0 to M2-Planet <stikonas>then currently you can only build mes from 32-bit stage0-posix <stikonas>(that migth change in the next release of mes, though probably will start with amd64) <stikonas>probie: though even stage0-posix arm64 support might benefit from some improvements if somebody is willing to do some work <fossy>IMO, if you are approaching bootstrapping from a trust perspective, you need to define well WHAT your trust goals are (for example, one of the reasons i like bootstrapping, is greatly minimising the infrastructure i have to trust in all the seed binaries) <fossy>i don't think it's reasonable for any one person to ever have complete trust though. modern systems have far too much code for someone to ever audit individually <fossy>and ofc, there are many reasons for bootstrapping outside of simply trust <probie>Is there any sort of plan to cut tcc out and have mes directly compile gcc? <janneke>feel free to go work on that, for the coming years i have other priorities <fossy>probie: perhaps in the very long term, but that would be a *LOT* of work <fossy>you'd have to tug both ways (simplifying gcc toward mes, but the much larger one, is expanding the constructs of mes toward gcc) <janneke>also, mes would have to change from an intepreter into a (pretty good) compiler, tcc is possibly two orders of magnitude faster than mescc <river>probie: is there a reason to want to do that? <roconnor>FlaminWalrus: Do we have a free formal spec for (a subset of) x86 available? I'm aware that the CompCert folks have one, but it didn't look free when I glanced at it. <stikonas>probie: what might make sense is cutting old tcc from the boot chain and going straight for the newer <stikonas>but I don't know how much work on mes side that would need <stikonas>I don't think mescc has been gaining any new features recently <stikonas>possibly at the exception of support for new arches <janneke>there have been a few bugfixes but mescc hasn't been touched, really, since it first built a working (bootstrappable-)tcc <stikonas>and for now we are waiting for other tings to land in mes 0.25 anyway... <janneke>ACTION just hopes that as mes matures, work on/contributing to mescc becomes even easier <fossy>x86 is not the architecture to use for trusted hardware <roconnor>Oh right, we could do risc-V or something. <probie>river: one fewer moving part, and possibly less work to support new architectures <stikonas[m]>You really need something that is far more standard than mescc <stikonas[m]>tcc is supported reasonably well by old GNU software and autotools scripts <probie>Should I be able to build mes with an amd64 M2-Planet, or does it need to be an x86 one? <probie>That seems to be a no, since there's no /lib/linux/x86_64-mes-m2 <probie>The x86_64-mes is broken, but should still be buildable, right? (just not via M2-Planet) <stikonas[m]>probie: there is some branch in mes that has better support <stikonas[m]>I once tried to get mes-m2 built with M2libc but it's hard... <stikonas[m]>mes.c uses quite a few helper functions and in meslibc headers they are quite intertwined with standard C functions <stikonas[m]>so you can't just replace core C library stuff with M2libc (e.g. fputs) and use mes helper functions from meslibc <stikonas[m]>in principle it would be much cleaner if we could build mes-m2 binary with M2libc C library <stikonas[m]>that would immediately port mes-m2 to all platforms that stage0-posix supports... <janneke>probie: x86_64-mes is broken in that it cannot build a bootstrappable-tcc that can compile itself <janneke>could also be a problem with bootstrappable-tcc <FlaminWalrus>fossy: if you can audit your way up to a formal proof-checker trusted core, then you can trust other people's formal correctness proofs in that proof language (and any other proof language that's provably-correctly-translated into that proof language) <FlaminWalrus>This requires people to actually write formal proofs though <roconnor>I'm skeptical this will ever happen with UNIX or *nix or whatever it is called. <FlaminWalrus>roconnor: not x86_64, but the seL4 whitepaper says Fox and Myreen, 2010 have L3 specs for (some version of?) RISC-V and ARM <probie>sanity check, if I'm running M2-Planet in bootstrap mode, should it be completely ignoring preprocessor directives? <FlaminWalrus>roconnor: in my opinion, microkernels are just better, and there's already one formally verified <FlaminWalrus>Very bare-bones, though, but they've shown it's at least possible to verify substantial, systems-level software <FlaminWalrus>Very nice and efficient IPC and cap-based security, extensive results on security properties, memory safety, lack of runtime errors, etc <stikonas[m]>probie: yes, bootstrap mode has no preprocessor directives except for nonstandard // CONSTANT <muurkha_>FlaminWalrus: Metamath Zero is a proof checker written with that in mind <muurkha_>roconnor: a problem with doing the bootstrap f <muurkha_>roconnor: a problem with doing the bootstrap <muurkha_>roconnor: a problem with doing the bootstrap on RISC-V is that older versions of GCC can't emit RISC-V code <roconnor>well we need to write our own free version of compcert's c compiler anyways ... <stikonas>yes, but risc-v support can be backported <stikonas>and binutils is not a problem as tcc can build 2.30 easily <stikonas>and risc-v is supported from at least 2.28 <janneke>stikonas: ah good question, i'm not 100% sure <stikonas>janneke: there are some build issues with kaem files on wip-x86_64 branch... <janneke>ACTION hasn't looked for a while (prolly while rebasing all the time) <stikonas>I think in other branches bootstrap mode might be gone <janneke>stikonas: ah, i think --bootstrap-mode has been obsoleted <stikonas>it looks like most commits are in (remove bootstrap mode from C files) <stikonas>so hopefully it's just kaem file that is old <probie>oh, I should have mentioned that I noticed that (hence my earlier question about bootstrap mode) <janneke>ACTION found 11d024e0 kaem.run: Remove --bootstrap-mode. <janneke>it seems that the stat64 and friends fix was rebased onto and i carelessly dropped that patch <stikonas>oh well, at least we now know that it is slightly broken <stikonas>janneke: while you are here, it would be helpful for builder-hex0 if we unify base-addresses in stage0-posix and mes <stikonas>let me check if we can just have a variable in kaem file <stikonas>because in stage0-posix different arches also have different base addresses <stikonas>can we move it as a variable to arch specific files? <stikonas>and ideally use the same value as in stage0-posix <stikonas>e.g. 0x8048000 instead of 0x1000000 on x86 <stikonas>builder-hex0 has no support for arbitrary base-address and needs it hardcoded <stikonas>right now we need to run "replace --file kaem.run --output kaem.run --match-on 0x1000000 --replace-with 0x8048000" to build mes on builder-hex0 kernel <stikonas>it's not particularly hard, but it's an extra step that could be eliminated <janneke>stikonas: sure, we can move that to a variable in kaem.<arch> files <janneke>and i can check if the change causes any problems (guess it shouldn't make any difference, but you never know) <janneke>(isn't that a terrrible address for debugging? anyway...) <stikonas>yeah, I'm not sure why stage0-posix-x86 uses it <stikonas>but it's harder to change it in hex code... <stikonas>as for amd64, in the latest git version of stage0-posix-amd64 base address doesn't matter at all <stikonas>M2-Planet now generates position independent (relocatable) assembly <stikonas>so quite a lot of things are still missing :( <janneke>right, that hasn't been rebased (on de rebase-failed wip branch), fun! <oriansj>well the reason why 0x8048000 was used, is that was the default address used by the assembler I was using to figure things out. And moving the hex0, hex1 and hex2 programs to a new base address would only be a dozen lines being changed. <oriansj>The hex0 programs that use the stack for the read/write syscalls and a register for the hold value don't need any absolute address. <oriansj>hex1 only needs 1 address (The label of addresses for the labels) and 2 references to it <oriansj>hex2 would only need 1 address to point to the struct list of labels and everything after that doesn't care <stikonas>oriansj: yes, but it's not just hex0, we also need to move builder-hex0 <stikonas>so we could probably change 08048000 to 10000000 fairly easily <stikonas>oh but mes uses 1000000 with one fewer 0 <stikonas>and this is already reserved in builder-hex0 for 01000000 - 0100000F stdin disk locato <stikonas>so we could make it slightly rounder figure, but ideally not too far from 08000000 <oriansj>fair enough, I don't think it is that serious of a problem but if someone cares enough to change it; I'll be more than happy to merge it. <stikonas>as 01000000 is too small for builder-hex0