Pagkatapos ng dalawang taon, bumalik ako sa blog para sa isang post na naiiba sa karaniwang nakakainip na mga lektura tungkol sa Haskell at matematika. Nagtatrabaho ako sa fintech sa EU sa nakalipas na ilang taon at tila dumating na ang oras upang magsulat tungkol sa isang paksa na hindi gaanong nakatanggap ng pansin mula sa tech media.
Inilabas kamakailan ng Facebook ang tinatawag nitong "bagong platform ng mga serbisyo sa pananalapi" na tinatawag na Libra. Ito ay nakaposisyon bilang isang digital settlement system batay sa isang basket ng mga internasyonal na pera na pinamamahalaan sa isang "blockchain" at nakaimbak sa isang money pool na pinamamahalaan mula sa Switzerland. Ang mga layunin ng proyekto ay ambisyoso at nangangailangan ng malakihang geopolitical na kahihinatnan.
Π ΠΈ Napakaraming makatwirang artikulo tungkol sa hindi wastong pananalapi at pang-ekonomiyang pagpapalagay sa likod ng iminungkahing sistema ng pananalapi. Ngunit walang sapat na mga espesyalista na may kakayahang mag-analisa mula sa isang teknikal na punto ng view. Hindi maraming tao ang nagtatrabaho sa imprastraktura sa pananalapi at nagsasalita sa publiko tungkol sa kanilang trabaho, kaya ang proyektong ito ay hindi nakakakuha ng maraming saklaw sa tech media, bagama't ang mga panloob nito ay bukas sa mundo. Ang ibig kong sabihin ay open source sa mga repository ΠΈ .
Ang bukas sa mundo ay isang architecturally schizophrenic artifact na sinasabing isang secure na platform para sa pandaigdigang imprastraktura ng pagbabayad.
Kung sumisid ka sa base ng code, ang aktwal na pagpapatupad ng system ay ganap na nag-iiba mula sa nakasaad na layunin, at sa mga pinaka-kakaibang paraan. Sigurado ako na ang proyektong ito ay may kawili-wiling kasaysayan ng kumpanya. Kaya't lohikal na ipagpalagay na ito ay idinisenyo nang may ilang sipag, ngunit sa katotohanan ay nakikita ko ang isang talagang kakaibang hanay ng mga desisyon sa arkitektura na sumisira sa buong system at naglalagay sa mga user sa panganib.
Hindi ako magpapanggap na may layunin na opinyon tungkol sa Facebook bilang isang kumpanya. Ilang tao sa industriya ng IT ang tumitingin sa kanya nang may simpatiya. Ngunit ang paghahambing ng mga pahayag nito at ang nai-publish na code ay malinaw na nagpapakita na ang nakasaad na layunin ay sa panimula ay mapanlinlang. Sa madaling salita, hindi binibigyang kapangyarihan ng proyektong ito ang sinuman. Mananatili siyang ganap na nasa ilalim ng kontrol ng isang kumpanya na ang negosyo sa advertising ay nabaon sa iskandalo at katiwalian na wala itong pagpipilian kundi subukang pag-iba-ibahin ang mga pagbabayad at credit scoring nito upang mabuhay. Ang malinaw na pangmatagalang layunin ay kumilos bilang isang data broker at tagapamagitan sa pag-access ng mga consumer sa credit batay sa kanilang personal na data ng social media. Ito ay isang ganap na kasuklam-suklam at madilim na kuwento na hindi nakakakuha ng atensyon na nararapat.
Ang tanging nakapagliligtas na biyaya ng kuwentong ito ay ang artifact na kanilang nilikha ay napakasayang hindi angkop sa gawaing nasa kamay na maaari lamang itong makita bilang isang gawa ng pagmamalaki. Mayroong ilang mga pangunahing error sa arkitektura sa proyektong ito:
Ang Paglutas sa Problema ng Byzantine Generals sa isang Access Control Network ay isang Pabagu-bagong Disenyo
Ang problema ng mga heneral ng Byzantine ay isang medyo makitid na lugar ng pananaliksik ng mga ipinamamahaging sistema. Inilalarawan nito ang kakayahan ng isang network system na makatiis ng mga random na component failure habang nagsasagawa ng mga corrective action na kritikal sa pagpapatakbo ng system. Ang isang nababanat na network ay dapat makatiis sa ilang uri ng pag-atake, kabilang ang mga pag-restart, pagkawala, malisyosong pag-load, at malisyosong pagboto sa mga halalan sa pamumuno. Ito ang pangunahing desisyon para sa arkitektura ng Libra, at ito ay ganap na walang kahulugan dito.
Ang overhead ng pagiging kumplikado ng oras ng karagdagang istrukturang ito ay nakasalalay sa algorithm. Maraming literatura sa mga variant ng Paxos at Raft protocol na lumulutas sa problema ng mga heneral ng Byzantine, ngunit lahat ng mga istrukturang ito ay nagpapakilala ng karagdagang overhead para sa komunikasyon 
upang mapanatili ang korum. Para sa Libra, pumili sila ng algorithm na may pinakamataas na posibleng gastos sa komunikasyon sa kaso ng pagkabigo sa pamumuno. At mayroong karagdagang overhead mula sa potensyal na muling halalan ng mga pinuno sa maraming uri ng mga kaganapan sa pagkabigo sa network.
Para sa isang system na tumatakbo sa loob ng isang consortium ng lubos na kinokontrol na mga multinasyunal na korporasyon, kung saan ang lahat ng mga user ay may code na nilagdaan ng Facebook at ang access sa network ay kinokontrol ng Facebook, ito ay sadyang walang saysay na isaalang-alang ang mga malisyosong kalahok sa antas ng pinagkasunduan. Hindi malinaw kung bakit lulutasin pa ng sistemang ito ang problema ng mga heneral ng Byzantine, sa halip na magpanatili lamang ng pare-parehong audit trail upang suriin ang pagsunod. Ang posibilidad ng isang Libra node na pinapatakbo ng Mastercard o Andressen Horrowitz na biglang nagsimulang magpatakbo ng malisyosong code ay isang kakaibang senaryo na dapat planuhin at mas mahusay na matugunan sa pamamagitan lamang ng pagtiyak sa integridad ng protocol at hindi teknikal (i.e. legal) na paraan.
Sinisingil ng testimonya sa Kongreso ang produkto bilang isang katunggali sa mga bagong internasyonal na protocol ng pagbabayad gaya ng WeChat, Alipay at M-Pesa. Gayunpaman, wala sa mga sistemang ito ang idinisenyo upang tumakbo sa mga validator pool upang malutas ang problema ng mga heneral ng Byzantine. Idinisenyo lamang ang mga ito sa isang tradisyunal na high-bandwidth na bus na gumagawa ng mga wiring ayon sa isang nakapirming hanay ng mga panuntunan. Ito ay isang natural na diskarte sa pagdidisenyo ng isang sistema ng pagbabayad. Mahusay na dinisenyo ang sistema ng pagbabayad ay hindi makakatagpo ng problema ng dobleng paggasta at mga tinidor.
Ang overhead ng consensus algorithm ay hindi malulutas ang anumang problema at nililimitahan lamang ang throughput ng system nang walang dahilan maliban sa cargo kulto ng pampublikong blockchain, na hindi nilayon para sa use case na ito.
Walang privacy sa transaksyon ang Libra
Ayon sa dokumentasyon, ang sistema ay dinisenyo na isinasaalang-alang pseudonymity, ibig sabihin, ang mga address na ginamit sa protocol ay nakuha mula sa mga pampublikong key sa elliptic curve at hindi naglalaman ng metadata tungkol sa mga account. Gayunpaman, wala saanman sa paglalarawan ng istraktura ng pamamahala para sa organisasyon o sa mismong protocol na ito ay nagpapahiwatig kung paano itatago ang data ng ekonomiya na kasangkot sa mga transaksyon mula sa mga validator. Ang system ay idinisenyo upang kopyahin ang mga transaksyon sa isang malaking sukat sa isang hanay ng mga panlabas na partido na, sa ilalim ng umiiral na European at US bank secrecy batas, ay hindi dapat malaman ang mga detalye ng ekonomiya.
Mahirap i-coordinate ang mga patakaran sa data sa iba't ibang bansa, lalo na dahil sa magkakaibang mga batas at regulasyon sa iba't ibang hurisdiksyon na may iba't ibang kultural na pananaw sa proteksyon at privacy ng data. Ang protocol mismo ay sa pamamagitan ng default ay ganap na bukas sa mga miyembro ng consortium, na isang malinaw na teknikal na pagkukulang na hindi nakakatugon sa mga kinakailangan kung saan ito idinisenyo.
Ang Libra HotStuff BFT ay hindi makamit ang throughput na kinakailangan para sa isang sistema ng pagbabayad
Sa UK, ang mga clearing system tulad ng BAC ay may kakayahang pangasiwaan ang humigit-kumulang 580 mga transaksyon bawat buwan. Kasabay nito, ang lubos na na-optimize na mga system tulad ng Visa ay maaaring magproseso ng 000 mga transaksyon bawat araw. Nag-iiba-iba ang performance depende sa laki ng transaksyon, pagruruta ng network, pag-load ng system, at (anti-money laundering, money laundering scheme).
Sinusubukan ng Libra na lutasin ang mga problema na hindi naman talaga problema para sa mga domestic transfer, dahil ang mga nation state ay na-moderno ang kanilang imprastraktura sa paglilinis sa nakalipas na dekada. Para sa mga retail na mamimili sa European Union, ang paglipat ng pera ay hindi isang problema. Sa tradisyunal na imprastraktura, maaari itong gawin gamit ang isang karaniwang smartphone sa loob ng ilang segundo. Para sa malalaking paglilipat ng korporasyon, mayroong iba't ibang mekanismo at panuntunan na nauugnay sa paglipat ng malalaking halaga ng pera.
Walang teknikal na dahilan kung bakit hindi rin mapoproseso kaagad ang mga pagbabayad sa cross-border, maliban sa mga pagkakaiba sa mga panuntunan at kinakailangan sa pagitan ng mga nauugnay na hurisdiksyon. Kung ang mga kinakailangang hakbang sa pag-iwas (customer due diligence, mga pagsusuri sa mga parusa, atbp.) ay ginawa nang maraming beses sa iba't ibang yugto ng chain ng transaksyon, maaari itong magresulta sa pagkaantala sa transaksyon. Gayunpaman, ang pagkaantala na ito ay isang function lamang ng regulasyong batas at pagsunod, hindi teknolohiya.
Para sa mga consumer, walang dahilan kung bakit hindi malilinaw ang isang transaksyon sa UK sa loob ng ilang segundo. Ang mga transaksyon sa tingian sa EU ay talagang bumagal (Know Your Customer) at mga paghihigpit sa AML na ipinataw ng mga pamahalaan at regulator, na pantay na nalalapat sa mga pagbabayad sa Libra. Kahit na malampasan ng Facebook ang mga hadlang sa mga paglilipat ng cross-border at pribadong paglilipat ng data, ang iminungkahing modelo ay daan-daang taong-taon ang layo mula sa pandaigdigang throughput ng transaksyon at malamang na kailangang muling idisenyo mula sa simula.
Mali ang wika ng Libra Move
Ang puting papel ay gumagawa ng mga matapang na pahayag tungkol sa isang bago, hindi pa nasusubukang wika na tinatawag na Move. Ang mga pahayag na ito ay medyo kahina-hinala mula sa punto ng view ng programming language theory (PLT).
Ang Move ay isang bagong programming language para sa pagpapatupad ng custom na transaction logic at smart contract sa Libra blockchain. Dahil nilalayon ng Libra na balang araw magsilbi sa bilyun-bilyong tao, idinisenyo ang Move na may seguridad bilang pangunahing priyoridad.
Ang isang pangunahing tampok ng Move ay ang kakayahang tukuyin ang mga arbitrary na uri ng mapagkukunan na may mga semantika na inspirasyon ng linear logic.
Sa mga pampublikong blockchain, ang mga matalinong kontrata ay nahaharap sa lohika ng mga pampublikong network na may mga escrow account, money laundering, OTC token issuance, at pagsusugal. Ginagawa ang lahat ng ito sa isang nakamamanghang hindi magandang disenyong wika na tinatawag na Solidity, na mula sa isang akademikong pananaw ay ginagawang parang henyo ang may-akda ng PHP. Kakatwa, ang bagong wika mula sa Facebook ay tila walang kinalaman sa mga teknolohiyang ito, dahil ito ay talagang isang scripting language na inilaan para sa mga hindi kilalang layunin ng negosyo.
Sa mga pribadong ibinahagi na ledger, ang mga matalinong kontrata ay isa sa mga terminong itinapon ng mga consultant nang hindi isinasaalang-alang ang malinaw na kahulugan o layunin. Karaniwang kumikita ang mga consultant ng software ng enterprise mula sa kalabuan, at ang mga matalinong kontrata ay ang apotheosis ng corporate obscurantism dahil maaari silang tukuyin bilang literal na anuman.
Pagkatapos mag-claim tungkol sa seguridad nito, kailangan nating tingnan ang semantika ng wika. Ang kawastuhan sa teorya ng programming language ay karaniwang binubuo ng dalawang magkaibang patunay: "progress" at "preservation", na tumutukoy sa pagkakapare-pareho ng buong espasyo ng mga panuntunan sa pagsusuri para sa wika. Higit na partikular, sa teorya ng uri, ang isang function ay "linear" kung ginagamit nito ang argumento nito nang eksaktong isang beses, at "affine" kung ginagamit ito nang higit sa isang beses. Ang linear type system ay nagbibigay ng static na garantiya na ang isang ipinahayag na linear na function ay tunay na linear sa pamamagitan ng pagtatalaga ng mga uri sa lahat ng function subexpression at pagsubaybay kung saan ginawa ang mga tawag. Ito ay isang banayad na pag-aari upang patunayan at hindi madaling ipatupad para sa isang buong programa. Ang linear na pag-type ay isa pa ring napaka-akademikong larangan ng pag-aaral, na naiimpluwensyahan ng pagpapatupad ng uri ng uniqueness sa Clean at type ownership sa Rust. Mayroong ilang mga paunang panukala para sa pagdaragdag ng mga linear na uri sa Glasgow Haskell Compiler.
Ang pahayag ng Move tungkol sa paggamit ng mga linear na uri ay tila isang hindi nararapat na pagsisid sa compiler, dahil doon . Sa abot ng masasabi ng isa, binanggit ng whitepaper ang kanonikal na panitikan mula kay Girard at Peirce, at walang katulad sa aktwal na pagpapatupad.
Bukod pa rito, ang mga pormal na semantika ng diumano'y secure na wika ay hindi lumalabas sa alinman sa pagpapatupad o sa dokumento. Ang wika ay sapat na maliit upang makahanap ng kumpletong patunay ng tamang semantika sa Coq o Isabelle. Sa katotohanan, ang isang end-to-end full conversion compiler na may proof transfer sa bytecode ay lubos na posible na ipatupad gamit ang mga modernong tool na naimbento noong nakaraang dekada. Alam namin kung paano gawin ito, simula sa noong 1996.
Mula sa pananaw ng teorya ng programming language, imposibleng subukan ang pag-aangkin na ang Move ay isang maaasahan at secure na wika, dahil ang mga claim na ito ay katumbas ng purong hand-waving at marketing kaysa sa aktwal na ebidensya. Ito ay isang nakababahala na sitwasyon para sa isang proyekto sa wika na hinihiling na iproseso ang bilyun-bilyong dolyar ng mga transaksyon.
Ang Libra cryptography ay may depekto
Ang pagbuo ng mga secure na cryptosystem ay isang napakahirap na problema sa engineering, at palaging pinakamahusay na lumapit sa pagtatrabaho gamit ang mapanganib na code na may isang mahusay na dosis ng malusog na paranoia. May mga pangunahing tagumpay sa lugar na ito, tulad ng proyekto ng Microsoft Everest, na bumubuo ng isang nabe-verify na secure . Umiiral na ang mga tool upang lumikha ng mga nabe-verify na primitive. Bagama't ito ay mahal, malinaw na hindi ito lampas sa mga kakayahan sa ekonomiya ng Facebook. Gayunpaman, nagpasya ang koponan na huwag lumahok sa proyekto, na inihayag bilang isang maaasahang pundasyon para sa pandaigdigang sistema ng pananalapi.
proyekto ng libra mula sa ilang medyo bagong mga aklatan para sa paglikha ng mga eksperimentong cryptosystem na lumitaw lamang sa nakalipas na ilang taon. Imposibleng sabihin kung ligtas o hindi ang mga dependency sa mga sumusunod na tool, dahil wala sa mga library na ito ang na-audit at walang mga karaniwang patakaran sa pagsisiwalat. Sa partikular, para sa ilang mga pangunahing aklatan ay walang katiyakan tungkol sa proteksyon laban sa mga pag-atake sa side-channel at pag-atake sa timing.
Ang library ng libra ay nagiging mas eksperimental at higit pa , paglalapat ng napakabagong mga diskarte tulad ng mga verifiable random function (VRF), mga pares ng bilinear, at mga lagda ng threshold. Maaaring makatwiran ang mga pamamaraan at aklatan na ito, ngunit ang pagsasama-sama ng lahat sa isang sistema ay nagdudulot ng malubhang alalahanin tungkol sa lugar ng pag-atake. Ang kumbinasyon ng lahat ng mga bagong tool at diskarteng ito ay lubos na nagpapataas sa pagiging kumplikado ng pagpapatunay ng seguridad.
Dapat ipagpalagay na ang buong cryptographic stack na ito ay mahina sa iba't ibang pag-atake hanggang sa mapatunayan kung hindi. Ang sikat na 'Move Fast and Break Things' na modelo ng Facebook ay hindi mailalapat sa mga cryptographic na tool na nagpoproseso ng data ng pananalapi ng customer.
Nabigo ang Libra na ipatupad ang mga mekanismo ng proteksyon ng consumer
Ang isang natatanging tampok ng sistema ng pagbabayad ay ang kakayahang ibalik ang isang transaksyon kung ang pagbabayad ay kinansela ng isang demanda o humantong sa isang aksidente o pagkabigo ng system. Ang sistema ng Libra ay idinisenyo upang maging "kumpleto" at hindi kasama ang isang uri ng transaksyon para sa pagkansela ng pagbabayad. Sa UK, ang lahat ng pagbabayad sa pagitan ng Β£100 at Β£30,000 ay napapailalim sa Consumer Credit Act. Nangangahulugan ito na ang sistema ng pagbabayad ay nagbabahagi ng responsibilidad sa nagbebenta kung sakaling magkaroon ng problema sa biniling produkto o kung ang tatanggap ng pagbabayad ay hindi nagbibigay ng serbisyo. Nalalapat ang mga katulad na panuntunan sa EU, Asia at North America.
Ang kasalukuyang disenyo ng Libra ay walang kasamang protocol upang sumunod sa mga batas na ito at walang malinaw na plano para sa paglikha nito. Mas masahol pa, mula sa pananaw ng arkitektura, ang finality ng authenticated data structure ng kernel, batay sa estado ng Merkle drive, ay hindi nagpapahintulot para sa anumang mekanismo na lumikha ng naturang protocol nang hindi muling idinisenyo ang kernel.
Pagkatapos magsagawa ng teknikal na pagsusuri ng proyektong ito, maaari nating tapusin na hindi ito papasa sa anumang respetadong distributed systems research o financial engineering journal. Upang subukang baguhin ang pandaigdigang patakaran sa pananalapi, isang malaking halaga ng teknikal na gawain ang kailangang gawin upang lumikha ng isang maaasahang network at secure na pagproseso ng data ng user na mapagkakatiwalaan ng publiko at mga regulator.
Wala akong nakikitang dahilan para maniwala na ginawa ng Facebook ang kinakailangang gawain sa disenyo nito upang madaig ang mga teknikal na problemang ito o na mayroon itong anumang teknikal na bentahe sa kasalukuyang imprastraktura. Ang pagsasabi na ang isang kumpanya ay nangangailangan ng kakayahang umangkop sa regulasyon upang galugarin ang mga pagbabago ay hindi isang dahilan para hindi muna gawin ang mga ito.
Pinagmulan: www.habr.com