#asciilifeform | 2019-12-27

today I learned about spark (ada spark, not apache spark). and associated modules like libsparkcrypto

02:29

seems like a promising foundation for actually secure software.

02:32

i have the "i don't know enough yet" optimism of that, maybe muen/genode, and maybe an actually secure bitcoin client.

02:38

the problem of having trusted hardware to run it on still seems like a gaping hole.

~ 15 minutes ~

02:54

mike_c: at one time i was interested in subj; even swallowed the book. then cooled to it

02:54

snsabot

(trilema) 2018-01-17 asciilifeform: thing is, a sparkism is not a substitute for a 'fits-in-head'-correct routine.

02:55

imho mechanical massage of programs is desirable strictly when it does not, itself, demand added complexity / moving parts

02:56

hm, but, if you can fit-in-head and have provable guarantees, it seems a stronger building block for larger things built in components.

02:57

if I have a crypto library I can analyze, convince myself is correct, and I *know* cannot overflow, etc.

02:57

then I can eject it from my head to make room for other things

02:57

mike_c: that's ffa , as it is.

02:58

ffa?

02:59

mike_c: http://www.loper-os.org/?cat=49

03:00

mike_c: roughly 3y of asciilifeform, above. possibly you were at sea during this.

03:02

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'.

↖

03:02

this is cool. do you think there is no added benefit to the "provable" overlay on top of something like this?

03:02

ah

03:04

ok, this is awesome, but question I am curious to hear your opinion on -

03:04

mike_c: you may find this vintage thread on subj also interesting.

03:04

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'

03:04

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

03:05

there's a spark/ada runtime

03:05

so you don't need 100mb of gnarl to run

03:07

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.

03:07

mike_c: re hardware, is separate conv. depending on your application, can sometimes get away w/ using vintage / nic-less irons.

03:08

yes, agreed on the additional complexity.

03:08

hm. nic-less no good for bitcoin node.. (fine for client though)

03:09

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)

03:09

yes, that feels obvious.

03:09

indeed, but afaik no one yet properly pulled it off.

03:10

also, on proper OS, that could be the spark'd component that the other part has no access to

03:11

mike_c: i rec to read ch1 of ffa series, won't take long, to get a feel for the approach.

03:11

reading.

03:11

my hypothesis was that it is possible to write demonstrably-correct soft w/out heavy mechanical help.

03:13

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)

03:14

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.

03:17

ffa ain't limited to rsa, however; is general-purpose numerics-in-constant-spacetime kit.

03:18

*

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.

03:18

i was skeptical of the side channel claims at the top.. but halfway through am starting to believe

03:20

mike_c: good % of the work , went into deriving closed forms of e.g. karatsuba's algo, barrett's method, miller-rabin, etc.

03:21

the existing public literature -- was of ~0 help.

03:22

ditto the code of the existing public nu

03:22

numerics libs.

03:22

100% of what i found, was ~garbage.

03:24

*

asciilifeform will bbl. will happily answer any an' all q's mike_c may have re ffa, when come back.

03:29

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.

03:31

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.

↖

03:31

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.

03:40

verisimilitude

I'm slowly learning SPARK through a book, but I've yet to get the impression it's an appreciable addition to Ada.

03:42

the appreciable addition is constraints from what i can tell so far.

~ 16 minutes ~

03:58

i have much more reading to do.. thanks for the links ascii.

~ 8 hours 55 minutes ~

12:53

Hello

12:53

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

13:06

"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

13:06

an equivalence between the mask set and the chip in your possession down to a near-atomic level without simultaneously destroying the CPU."

~ 2 hours 50 minutes ~

15:56

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

~ 15 minutes ~

16:12

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.

↖

16:16

he's been peddling similar nonsense cocktails for many yrs.

16:27

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)

16:27

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.

16:30

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

16:31

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) .

16:33

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.

16:38

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 .

~ 3 hours 25 minutes ~

20:04

http://bingology.net/2019/data-center-survey-part-one-latam-and-iberia/ << Bingology - BingoBoingo's Blog -- Data Center Survey Part One - LATAM and Iberia

~ 28 minutes ~

20:32