<OriansJ>stikonas[m]: well unfortunately the only people currently funding the development of secure bootstraps are nation states and crypto-communities. <OriansJ>With nation states by far being the biggest backers. <xentrac>I think there are some other kinds of states funding them too, like the US <xentrac>I mean I know there's a movement to turn the US into a nation-state, and arguably it was a nation-state before the Civil War <OriansJ>xentrac: Well I am being funded by the State of Michigan (as my Day job and doing this for fun in my limited free time) <xentrac>but right now it's a polyethnic melting-pot state <xentrac>I'd say that's you funding it, not Michigan <xentrac>similarly, I don't think anyone is funding malina to come in here and sneer at us and shit on what we're doing <OriansJ>xentrac: well if the State of Michigan paychecks stop, My bootstrapping work gets put on hold until an alternative funding source could be obtained. <xentrac>I think he's doing that entirely on his own initiative <xentrac>yeah. but I mean for example the work I'm doing on Hammer (vaguely applicable) is funded by the DoD, part of the polyethnic state of the US <OriansJ>I assume everyone is motivated by self interest. <xentrac>That would be a pretty big improvement in my case <OriansJ>xentrac: some people want to feel good more than they want to make the world a better place. <xentrac>I think seL4 is mostly funded by Australia <OriansJ>xentrac: most people don't even know let alone care we exist and are doing what we are doing. <xentrac>they have a different defense against the Karger-Thompson attack, as far as it goes <OriansJ>xentrac: well shared work would have been cheaper and faster but oh well. <xentrac>which doesn't extend yet to compiling other software than the kernel <xentrac>Metamath, as I mentioned above, has another related angle <OriansJ>well xentrac seL4 isn't immune to the Karger-Thompson attack at all. Their proofs wouldn't prevent such a backdoor from being installed by the compiler. <xentrac>seL4's proofs *do* prevent such a backdoor from being installed by the compiler into the kernel <xentrac>early on they didn't, because they only covered the source code <xentrac>but at this point they're routinely verifying the kernel's machine code <OriansJ>xentrac: they didn't prevent C's undefined behavior from implementing a standard security vulnerability. <xentrac>are you saying there was a standard security vulnerability in the seL4 kernel, and that their proofs of the machine code were faulty? I haven't heard about this <OriansJ>Now they might have made improvements since I looked at it last year but proofs down to assembly they did not have. <siraben>with any such proof isn't there going to be a gap between reality and the model? <xentrac>Thompson's variant of the attack of course didn't backdoor the kernel at all; it backdoored the login program <xentrac>siraben: possibly; they need a model of the hardware's behavior, and the hardware might not follow that model <OriansJ>xentrac: backdooring the kernel makes backdorring everything so much simpler. <siraben>Right, the trust has to go below assembly level even, down to hardware <xentrac>and certainly with some probability the hardware will commit undetected bit errors, or leak information through covert channels you didn't account for <OriansJ>xentrac: I believe NASA has said to the effect, EVERY chip with more than 16pins deviates from the specification. <siraben>of course NASA would know all about hardware errors, being exposed to the radiation belts of Jupiter isn't exactly nice for hardware <xentrac>OriansJ: well, a nice thing about axiomatic reasoning like what seL4 is using is that their model doesn't have to specify everything <OriansJ>for example Intel's Documentation says NOP is 2, 4 and 6 bytes in length <xentrac>the things that it doesn't specify aren't permitted to be used in the proofs, so it doesn't matter what happens there <xentrac>the proof verifies that you don't stray from the well-lit path <OriansJ>siraben: I loved their GeAs on sapphire work; pity it never took off. <xentrac>it's true that the kernel is the most effective thing for an attacker to backdoor, but they still win if they backdoor the login program, as Thompson did <OriansJ>xentrac: sorry Gallium not Germanium <xentrac>I saw a proposal in #erights last week that reduces that problem substantially: instead of running a root sshd, run an sshd for each user, on a different port, as that user ID <siraben>CCC is about deriving a compiler directly from the semantics of the language <xentrac>that way there's no centralized "login" process that can be corrupted, and users can run their own versions --- although of course if they're all running a backdoored binary, that doesn't help :) <OriansJ>hoping that the software doesn't do something tricky to compromise it <fossy>xentrac: seL4 is funded by CSIRO which has a pretty large government grant <xentrac>fossy: thanks! I didn't remember which agencies were involved <fossy>it is a government agency, so hence gains the majority of funding from the government <xentrac>OriansJ: what's the benefit of the sapphire substrate? <xentrac>(it's cheaper than gallium arsenide, maybe?) <OriansJ>xentrac: well it is more radiation hardened and allows the use of Al2O3 as a gate oxide for GaAs. Not to mention much less fragile. but they never got past the 500nm process node. <OriansJ>The sort of process you would want if failure from a nuclear bomb blast or solar flare was unacceptable. <OriansJ>and Silicon on sapphire lost out to the much more common silicon on insulator process which lacks the radiation hardening aspects <remexre>somewhat the "wrong kind" of bootstrapping, but I've got a VM of a non-Linux Unix with gcc 3.3 on it; is there any hope of getting this to a recent gcc without a half-dozen intermediate versions? <remexre>tried going thru mes, but it failed because I can't build gmp 4.1 <OriansJ>remexre: it probably could do 4.7.4 and then it would be 3 steps to GCC-10 <OriansJ>So I guess the designed to survive the end of the world sort of properties does appeal to me. Although bunny's work on optical verification of circuits is kinda cool on a different level for me. (printed plastic transistors look like something fun to do) <pder>fossy: I have a fix in live-bootstrap for bash so it doesnt segfault. Should I base it on your bash-2.05b branch? <remexre>I guess I'll try gmp 4.2, maybe it fixes whatever's breaking 4.1 <remexre>(which involves M4, so I haven't dug into it...) <fossy>pder: wait for the restructure which is about to come <fossy>remexre: lol, i am interested to hear more about your usecase <fossy>siraben: pder restructure done <siraben>fossy: restructuring what again? I forgot <fossy>oops bad bing, sorry siraben <fossy>i meant to ping stikonas[m] (structure done) <remexre>fossy: I've been feeling like I'd prefer XNU to Linux, so I'm trying to get it out of my system by using Darwin in a VM for a few days <remexre>but it's been 15+ years since the last ISO release... <fossy>GCC may not compile all the way up to 10 on darwin, but you can try :) <remexre>yeah, I'm planning to switch to clang once I get something that does a recent enough C++ <remexre>oh wow, latest problem: they wrote their own ld in this release <fossy>what'd you expect, a GNU toolchain? :P <remexre>dunno why they wouldn't use binutils once they were bootstrapped <pder>fossy: restructure and readme look nice. I created a PR for the bash segfault ***mephista is now known as spicy_icecream
<fossy>pder: would you mind rebasing on the latest commit so CI happens? <fossy>actually nvm, i know that's right <fossy>gforce_de1977: ooh, yes i will ***mephista is now known as spicy_icecream
<siraben>What does the CI do here? Does it actually run the executables compiled? <stikonas[m]>I guess I'll need to rebase/adjust coreutils branch to new layout <fossy>siraben: it just runs the build <fossy>which does involve very basic checks <stikonas[m]>Well, most of the executables are used later in bootstrap, this is self testing project anyway ***ChanServ sets mode: +o rekado_
***rekado_ is now known as rekado
<stikonas>fossy: any reason why you now have src dirs with .placeholders in the repo instead of creating them in rootfs.sh? <stikonas>something is also broken cc_x86 hold M2.M1 fails to run... Probably some files have incorrect paths... <stikonas>anyway, I think we should either download into src dirs using get_file or download into /sources/ and copy into src dir in rootfs... <pder>stikonas: I am not able to reproduce that issue since the restructuring. Are you on commit 329afda94d6b5f412e43f? <pder>However, I was not able to update to get my submodules to update properly after updating to latest master. I ended up recloning <stikonas>but yeah, modules didn't update properly <pder>As a sanity check I would recommend recloning with git clone --recursive <pder>After coreutils, is perl next? <stikonas>I have started with heirloom yacc, but now I was rebasing... ***yt_` is now known as yt_
<OriansJ>stikonas: always make sure to do git submodule update --checkout to ensure the submodules are on the correct commit too. <yt_>OriansJ: good evening <OriansJ>I'm started to be tempted to add a block in cc_* to just show an error when given an empty input file <yt_>how's it going? sorry I haven't been around much for the last two weeks. it's been busy! <OriansJ>yt_: I know the feeling. like an endless stream of priority tasks that need attention immediately <yt_>OriansJ: exactly. in my case, dealing with two nasty performance regressions upstream, and a floorboard that needed mending XD <yt_>and somehow, an hour or two at a time never seems enough to make meaningful progress on something