IRC channel logs

<rickmasters>cosinusoidally: my suspicion is that it only appears to get stuck. I think its just hanging after the last attempt to print.

<rickmasters>cosinusoidally: I'm trying to narrow down where it is failing. Somewhere in tcc_add_file I think.

<oriansj>Mikaku: well no details on the firmware situation but you are not alone in using qwerty; but it looks about the right size for a young child.

<matrix_bridge><Andrius Štikonas> Probably u-boot. Possibly with some blobs other than BootROM

<rickmasters>cosinusoidally: Preliminary diagnosis is that builder-hex0 is not handling a read of length zero.

<rickmasters>cosinusoidally: This is where it originates: https://github.com/cosinusoidally/tcc_bootstrap_alt/blob/11053b220e492464fade120682ded105c5d95ead/tcc_27/tccelf.c#L2437

<rickmasters>cosinusoidally: builder-hex0 decrements the length after each byte and then checks for zero remaining. This won't work for zero lengths.

<rickmasters>cosinusoidally: I actually fixed this for writes but neglected to ensure reads didn't have the same problem.

<rickmasters>cosinusoidally: I'll fix builder-hex0 but I've confirmed thqt adding `if (size > 0)` to the line linked above fixes the problem

<rickmasters>cosinusoidally: fixed builder-hex0 has been pushed.

<euleritian>Ah! Very interesting! Are there unit tests for builder-hex0? This sounds like something quickcheck (https://hackage.haskell.org/package/QuickCheck) or hypothesis (https://hypothesis.readthedocs.io/en/latest/) should have found.

<Mikaku>oriansj: :-)

<euleritian>orians: How do you fuzz? Do you have a preferred setup and tools? After reading the wikipedia page I'd like to learn more.

<euleritian>From what I read, a lot of fuzzing requires compiling the target to be compiled with a special compiler. My hope is that guix can be of use here,

<muurkha>you can fuzz things without using a special compiler

<muurkha>some fuzzers do use a special compiler, others don't

<muurkha>the original fuzz paper just fed random bytes to standard Unix utilities and watched them crash

<muurkha>quickcheck is closely related to fuzz

<muurkha>I've used Hypothesis for fuzzing at times; this requires some trickery with fork to handle actual crash bugs

<nimaje>well, property based testing (quickcheck, Hypothesis) is related to fuzzing, you could even call it a generalisation, instead of random bytes you generate proper objects matching the types and you allow more general properties than "it does not crash"

<muurkha>fuzzing is more general than most property-based testers in one way, though: you can apply it to programs you know nothing about

<muurkha>I don't know if there's a way to get Hypothesis to run a program with an *infinite* stream of random bytes

<nimaje>you could probably misuse the RuleBasedStateMachine for that and set all limits to some big number, so it seems like infinite, but yeah, hypothesis is not meant for that

<oriansj>euleritian: I have been using https://github.com/vanhauser-thc/AFLplusplus (unfortunately guix doesn't have it packaged yet, so I have been using a debian system to do the fuzzing)

<oriansj>all one has to do is replace gcc with afl-gcc when building and then afl-fuzz -i examples/ -m 4G -o results/ -- bin/M1 --architecture x86 -f @@ to get it tested

<oriansj>for tools that haven't been fuzzed yet, you'll usually get crashes within a few seconds; after a few dozen run/fix cycles the time to crash grows longer and longer.

<oriansj>at this point, the time to finding a crash is longer than the time to add a new feature and start again. which is nice because no one has reported any crashes for a while now.

<muurkha>nimaje: oh, that's an excellent point

<musllll>Hello everyone, just found about stage0 and its related projects. I want to ask, out of curiosity, what is the current opinion of devs in regards to theorem proving and how it could 'free' us from the "Nexus Intruder attack" (as described by jeremiah)?

<musllll>High-assurance software has been using formal specification/proving for decades now. Some software, such as seL4 kernel, has been proved to be correct to the specification down to bit level, thus making a compiler attack impossible (hardware/firmware has not been proved, btw). It is, to my knowledge, the first software to receive EAL7+ ratings (above the maximum described by common criteria). Is this not a possible route to

<muurkha>dunno if I count as a dev but I think theorem proving may end up being a more powerful defense than the very useful and important stuff we already have

<muurkha>it's not really true in practice that high-assurance software has been using formal specification/proving for decades now. it's been aspiring to do so, which is why seL4 is the first EAL7+ kernel, rather than the thirtieth

<musllll>To cite another example, CompCert. Although it has not been fully verified, like seL4, it is still a great effort. Another example, CakeML. They recently built their own verified Verilog compiler, called Lutsig.

<muurkha>yeah, I think that stuff is really interesting and important, and Metamath shows a convincing way to counter potential attacks on the theorem prover itself

<muurkha>CompCert and seL4 are really exciting developments, and formal methods are seeing a lot more uptake now then ten or twenty years ago

<musllll>@murrkha it is true though... formal verification has been done for at least 30 years now, although is a way more rudimentary way than current automated theorem provers like Z3 and Isabelle HOL

<muurkha>it started in the 60s, more than 50 years ago

<muurkha>but until the last few years was not able to scale up to practical systems

<muurkha>seL4 relatively recently (four years ago?) upgraded their proofs to cover not just the C source code but also the executable output from untrusted compilers

<muurkha>not, of course, *all* untrusted compilers. just the ones they happen to be using at the moment

<musllll>@muurkha I'm not familiar with the project/person you mentioned (Metamath), could you tell me where to find it?

<nimaje> https://us.metamath.org/

<musllll>yes, just saw that, but i meant the part where it shows attacks on theorem provers itself

<nimaje>well, you have a detailed proof certificate and afaik there are multiple checkers

<muurkha>it doesn't show attacks on them; it shows how to make attacks on them impossible

<musllll>oh i see, i misunderstood your previous comment about metamath... but yes, exactly my point, formal proof can be used to escape the trusting trust problem which is one of the main points of stage0

<muurkha>I think so, yeah

<muurkha>I mean you still need trustworthy hardware to run your metamath verifier on, and some way to get the purported proof certificate onto it, and enough UI to see what theorem it is that you're verifying, and some reasonable assurance that the hardware you're running on has the behavior your proof assumes

<muurkha>seL4 had to be patched for Spectre and Meltdown

<janneke>ACTION is working on https://dezyne.org -- not really theorem proving but rather automagical application of formal methods

<stikonas>janneke: at some point when you have time could you also review https://lists.gnu.org/archive/html/bug-mes/2024-01/msg00009.html

<stikonas>I've sent a patch yesterday

<janneke>stikonas: sure, great work!

<muurkha>fantastic!

<muurkha>is https://dezyne.org/dezyne/manual/dezyne/html_node/Introduction.html the place to start, janneke?

<stikonas>I have tried rebuilding mes with mes-m2 and it worked and the resulting binary was fine

<stikonas>haven't tried building tcc-mes yet but x86_64 bootstrap of tcc was never finished anyway

<janneke>that's great and yes, indeed

<stikonas>probably should try to finish off that x86_64 mes->tcc step too at some point when I find some time

<stikonas>I suspect it's very close given that we sorted out most 64-bit bugs with riscv64 bootstrap

<janneke>exactly, i'd hope/think that too

<janneke>muurkha: yes, sure

<janneke>there will (finally) be a talk about dezyne at fosdem this year -- https://fosdem.org/2024/schedule/event/fosdem-2024-1872-how-to-create-the-universal-operating-system/

<muurkha>wonderful!

<janneke>(the aspirations are much higher than the actual state of affairs, as always ;)

<muurkha>the only way to avoid that is to have terrible aspirations

<janneke>hehe, true

<stikonas>hmm, there is something in mes-m2 that upsets posix-runner after I run it 30 times or so in kaem script. Yet full mes seems to be fine

<stikonas>oh that probably makes sense, that's because mes libc has a trivial free() function

<stikonas>so even if posix-runner breaks something, it's not triggered by free

<matrix_bridge><cosinusoidally> @irc_libera_rickmasters:stikonas.eu: Thanks, the fixed builder-hex0 works for me. I might not be invoking qemu correctly, but it gets stuck at the fiwix trampoline. Any ideas on the issue with cdrun? I'm guessing it might be something to do with me using exec rather than fork+exec?

<musllll>@muurkha sorry for the late reply... you don't need to verify it inside the system you're running btw, you can just ship the binary already verified.

<musllll>dezyne looks really interesting, i'll take a look

<musllll>btw, has anybody yet made TCC compile at least some old GCC yet? Or is GCC not required at all to build something like linux kernel?

<musllll>I saw the builder-hex0 project, which seems to do exactly that, but it was not clear if it uses TCC or compiles GCC using stage0-produced binaries

<stikonas>musllll: tcc can compile gcc

<stikonas>and gcc is required to build linux kernel

<stikonas>but you don't need linux kernel to run gcc

<stikonas>so on bios systems you can use builder-hex0 to reach tcc and use it to build Fiwix kernel

<stikonas>then fiwix kernel is good enough to reach GCC an build somewhat older Linux

<stikonas>(could possibly be extended to build newer stuff but there are various limitations, especially if you want to keep bootstrap in the memory)

<stikonas>and this is all just on x86

<stikonas>I'm now working on some builder-hex0 alternative for UEFI/x86_64 systems

<stikonas>but we don't yet have amd64 bootstrap even on POSIX systems (i.e. exclude kernel bootstrap)

<musllll>lol i just now realized you're the author of the repository i was reading (stage0-uefi) haha... great work btw, i like'd you also added gentoo scripts to bootstrap rustc

<stikonas>yeah, I did that too

<musllll>did you take a look at oreboot? this is a bit unrelated to the current project, but RustSBI might be useful somehow

<stikonas>no, I haven't looked at oreboot...

<stikonas>I only have coreboot on one machine

<musllll>it's a minimal version of coreboot, written in rust: https://github.com/oreboot/oreboot

<stikonas>yeah, I've briefly heard it mentioned before

<musllll>just one more question: is stage0 and it's related project using some building system to ensure deterministic builds (such as Guix or Nix)?

<stikonas>you don't need anything special for deterministic builds

<stikonas>especially stage0-* stuff

<stikonas>it just doesn't have any non-deterministic input there

<musllll>but you guys have sha256 or something?

<stikonas>yes, we do have sha256

<stikonas>and we check outputs with it

<stikonas>there is also live-bootstrap

<stikonas>that builds further stuff after stage0-posix

<musllll>i see, thanks for answering my dumb questions :)

<stikonas>there we have to do occasional tricks for deterministic builds (but not too many)

<stikonas>so the interesting consequence of bootstrapping

<musllll>really excited about this project, i always got the idea to do something like that, but i lacked the expertise, you guys are awesome for actually doing it

<stikonas>is that you get reproducable builds almost for free

<stikonas>i.e. normally output of the binary depends on toolchain, etc...

<musllll>interesting

<stikonas>but here we have the whole chain built from a tiny hex0 binary

<musllll>it's also a good thing that there's no optimizing compiler doing heuristic stuff

<stikonas>yeah, GCC is deterministic...

<matrix_bridge><cosinusoidally> Looks like someone did once get a 4.6 Linux kernel built with tcc https://www.youtube.com/watch?v=iU0Z0vBKrtQ . I can't find the code online though.

<matrix_bridge><cosinusoidally> ah it's https://github.com/susematz/linux

<matrix_bridge><cosinusoidally> ah still depends on gcc https://github.com/susematz/linux/blob/tcc46/README.tcc

<fossy>cosinusoidally yeah i saw that before, it's a huge mess unfortunately

<fossy>snuik: tell musllll in the long term i do think that formal verification does have a role to play in the bootstrap story. but the cost & time expense required for formal verification of most software is immense (i think the figure i've seen quoted for seL4 is it took AU$2 mil?)

<snuik>Does not compute.

<fossy>snuik: help

<snuik>Don't ask me fossy, I'm just a bot!

<fossy>uh ok

<stikonas>fossy: you need to use "later tell"

<fossy>ahhhhh ok

<fossy>snuik: later tell musllll in the long term i do think that formal verification does have a role to play in the bootstrap story. but the cost & time expense required for formal verification of most software is immense (i think the figure i've seen quoted for seL4 is it took AU$2 mil?)

<snuik>Sure thing.

<fossy>thanks

<stikonas>and early hex0 programs are not formally verifiable

<stikonas>they have known crashes

<stikonas>there is basically no error handling

<stikonas>well, maybe you can restrict verification to good input...

<stikonas>fossy: quick question, should --arch be renamed to --architecture

<stikonas>rest of the options are not abbreviated...

<stikonas>right now it's probably still easy to rename since there are not real users of --arch

<stikonas>s/not/no

<fossy>stikonas: i guess so? adds a small amount of clarity without any harm. arch is a super common abbreviation but it doesn't hurt to change

<stikonas>hmm, on the other hand we have bwrap too

<stikonas>rather than full bubblewrap

<stikonas>though the command is also abbreviated...

<stikonas>ok, we actually have a few more

<stikonas>repo...

<stikonas>oh well, maybe it's fine...

<fossy>if they were uncommon abbreviations i'd instantly say yes, but i don't think there's a lack of clarity with any of them

<stikonas>oh well, let's leave as it is then

IRC channel logs

2024-01-20.log