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.
asciilifeform: mike_c: at one time i was interested in subj; even swallowed the book. then cooled to it
snsabot: (trilema) 2018-01-17 asciilifeform: thing is, a sparkism is not a substitute for a 'fits-in-head'-correct routine.
asciilifeform: imho mechanical massage of programs is desirable strictly when it does not, itself, demand added complexity / moving parts
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
asciilifeform: mike_c: that's ffa , as it is.
mike_c: ffa?
asciilifeform: mike_c: roughly 3y of asciilifeform, above. possibly you were at sea during this.
asciilifeform: mike_c: i went with ultra-pedantic 'by hand' proofs, raher than sparkism, for the reason that sparkism, like other mecha-proof systems, aint 'free', the various nudges the compiler demands, conceptually 'weigh' something, and interfere w/ 'fits in head'.
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: ah
mike_c: ok, this is awesome, but question I am curious to hear your opinion on -
asciilifeform: mike_c: you may find this vintage thread on subj also interesting.
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
asciilifeform: mike_c: re spark, it was hands-down the least objectionable of the various 'proof systems' i've used thus far. but it still 'weighs down' the text, spark does not operate on unmodified ada proggies.
asciilifeform: mike_c: re hardware, is separate conv. depending on your application, can sometimes get away w/ using vintage / nic-less irons.
mike_c: yes, agreed on the additional complexity.
mike_c: hm. nic-less no good for bitcoin node.. (fine for client though)
asciilifeform: mike_c: the mp people had, imho, the correct thrust there (i.e. cut node into 2 components, where only the smaller actually touches privkeys)
mike_c: yes, that feels obvious.
asciilifeform: indeed, but afaik no one yet properly pulled it off.
mike_c: also, on proper OS, that could be the spark'd component that the other part has no access to
asciilifeform: mike_c: i rec to read ch1 of ffa series, won't take long, to get a feel for the approach.
mike_c: reading.
asciilifeform: my hypothesis was that it is possible to write demonstrably-correct soft w/out heavy mechanical help.
asciilifeform: the series is ~complete (needs still ability to hash, to be deployable for practical rsaism; but can be used in fact as-is w/ external hashism even nao)
asciilifeform: my approach to rsa, was to derive a closed algebraic form for all of the necessary operations, so in fact can express'em w/out data-dependent branching or memory indexing. which thermonukes side-channelism, but as bonus also makes the algos '9000x' easier to analyze by hand.
asciilifeform: ffa ain't limited to rsa, however; is general-purpose numerics-in-constant-spacetime kit.
asciilifeform fwiw is satisfied that it is 100% correct, and would readily jump on a parachute made of it. but the cost was that it took >3y, and most of the orig. interested folx, at this pt have gone home.
mike_c: i was skeptical of the side channel claims at the top.. but halfway through am starting to believe
asciilifeform: mike_c: good % of the work , went into deriving closed forms of e.g. karatsuba's algo, barrett's method, miller-rabin, etc.
asciilifeform: the existing public literature -- was of ~0 help.
asciilifeform: ditto the code of the existing public nu
asciilifeform: numerics libs.
asciilifeform: 100% of what i found, was ~garbage.
asciilifeform will bbl. will happily answer any an' all q's mike_c may have re ffa, when come back.
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: Hello
amberglint: asciilifeform: I think you might find this amusing, someone famous in the open sores community wants to build "trustable hardware": https://www.bunniestudios.com/blog/?p=5706
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."
feedbot: http://qntra.net/2019/12/alphabets-youtube-takes-down-bitcoin-and-crypto-videos-before-quickly-restoring-them-as-irrelevant/ << Qntra -- Alphabet's Youtube Takes Down "Bitcoin and Crypto" Videos Before Quickly Restoring Them As Irrelevant
asciilifeform: amberglint: the huang fella is a вредитель , likely sponsored directly by the enemy. consider: with what it cost to bake his shitware to date, one could easily order a properly-open fpga made from 0. but instead he pushes xilinx's.
asciilifeform: he's been peddling similar nonsense cocktails for many yrs.
asciilifeform: http://logs.nosuchlabs.com/log/asciilifeform/2019-12-27#1004576 << adds ~appearance~ of correctness, rather than assurance. consider, the correctness of the mechanized analyzer per se, ultimately must be determined by hand (is it obvious why, or do i have to draw a picture..?) and afaik this has not been done for any such item (typically their sheer 'mass' , makes the proposition ~impossible)
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.
feedbot: http://qntra.net/2019/12/kansas-city-inmates-drastically-inflated-property-tax-payment-refused-by-whitney-for-being-wrong-type-of-usg-issued-scrip/ << Qntra -- Kansas City Inmate's Drastically Inflated Property Tax Payment Refused By Whitney For Being Wrong Type Of USG Issued Scrip
asciilifeform: the proper, imho, method to 'write correct crypto' , is demonstrated in my series : remove all data-dependent branches and memory indexing; simplify the algos (e.g. karatsuba without movable pivot) to the point where their correctness can be trivially shown by hand, on paper; and implement in lang w/ proper bounds-checking (ada) .
asciilifeform: some of the proofs, e.g. the space bound of barrett's method, are arguably painful to eat. but i (and coupla other folx, most of whom have unfortunately run off) satisfied that correct.
asciilifeform: mike_c: naively one might expect constant-spacetime (i.e. 1^1 mod 1 takes same time and memory, in particular bitness, as any other modular exp) would be ruinously slow; but in practice faster than heathen rsa routines, on acct of the peculiarities of current-day cpus .
feedbot: http://bingology.net/2019/data-center-survey-part-one-latam-and-iberia/ << Bingology - BingoBoingo's Blog -- Data Center Survey Part One - LATAM and Iberia
feedbot: http://bingology.net/2019/data-center-survey-part-2-poland-serbia-prague-with-its-outlying-areas/ << Bingology - BingoBoingo's Blog -- Data Center Survey Part 2: Poland, Serbia, Prague With Its Outlying Areas