mike_c: today I learned about spark (ada spark, not apache spark). and associated modules like libsparkcrypto
mike_c: seems like a promising foundation for actually secure software.
mike_c: i have the "i don't know enough yet" optimism of that, maybe muen/genode, and maybe an actually secure bitcoin client.
mike_c: the problem of having trusted hardware to run it on still seems like a gaping hole.
snsabot: (trilema) 2018-01-17 asciilifeform: thing is, a sparkism is not a substitute for a 'fits-in-head'-correct routine.
mike_c: hm, but, if you can fit-in-head and have provable guarantees, it seems a stronger building block for larger things built in components.
mike_c: if I have a crypto library I can analyze, convince myself is correct, and I *know* cannot overflow, etc.
mike_c: then I can eject it from my head to make room for other things
mike_c: this is cool. do you think there is no added benefit to the "provable" overlay on top of something like this?
mike_c: ok, this is awesome, but question I am curious to hear your opinion on -
snsabot: (trilema) 2018-11-29 asciilifeform: wtf is the point of 'here's a proof but you need this here 100MB of gnarl to ~run~ it and of course you will trust output, or are you a terrorist'
mike_c: it seems entirely possible, through that method, or sparkism, to build secure software. But it seems to me you are still hung on the cross of the hardware you have to run it on
mike_c: there's a spark/ada runtime
mike_c: so you don't need 100mb of gnarl to run
mike_c: yes, agreed on the additional complexity.
mike_c: hm. nic-less no good for bitcoin node.. (fine for client though)
mike_c: yes, that feels obvious.
mike_c: also, on proper OS, that could be the spark'd component that the other part has no access to
mike_c: i was skeptical of the side channel claims at the top.. but halfway through am starting to believe
verisimilitude: It's interesting, asciilifeform; I've been of the opinion that striving to write correct software should be the default and that a mechanical system on top of that is merely good for being doubly sure of the correctness.
mike_c: mechanical system adds assurance of correctness with the penalty of harder to fit-in-head and therefore being less sure of what it is correctly doing. an interesting dilemma.
verisimilitude: Now, I've been vaguely aware that you'd some manner of ``falling out'' with the trilema crowd, but I still hardly have an understanding of what transpired there. I do feel vindicated in my decision to not associate with them and use this channel, to associate with you, however.
verisimilitude: I'm slowly learning SPARK through a book, but I've yet to get the impression it's an appreciable addition to Ada.
mike_c: the appreciable addition is constraints from what i can tell so far.
mike_c: i have much more reading to do.. thanks for the links ascii.
amberglint: "While open hardware has the opportunity to empower users to innovate and embody a more correct and transparent design intent than closed hardware, at the end of the day any hardware of sufficient complexity is not practical to verify, whether open or closed. Even if we published the complete mask set for a modern billion-transistor CPU, this “source code” is meaningless without a practical method to verify
amberglint: an equivalence between the mask set and the chip in your possession down to a near-atomic level without simultaneously destroying the CPU."
snsabot: Logged on 2019-12-27 03:31:10 mike_c: mechanical system adds assurance of correctness with the penalty of harder to fit-in-head and therefore being less sure of what it is correctly doing. an interesting dilemma.