นับตั้งแต่เริ่มก่อตั้ง วิธีการตรวจสอบอย่างเป็นทางการ (Formal Verification) ได้เชื่อมโยงกับคำต่างๆ เช่น "เฉพาะกลุ่ม ไม่เป็นที่นิยม" บางคนกล่าวว่าวิธีการตรวจสอบอย่างเป็นทางการเป็นวิธีการต่อต้านการแฮ็ก "ระดับทหาร" ซึ่งเพิ่มความลึกลับให้กับเทคโนโลยีนี้

วิธีการตรวจสอบอย่างเป็นทางการคืออะไร?

Wikipedia อธิบายการยืนยันอย่างเป็นทางการดังนี้:

ในกระบวนการออกแบบฮาร์ดแวร์คอมพิวเตอร์ (โดยเฉพาะวงจรรวม) และระบบซอฟต์แวร์ ความหมายของการตรวจสอบอย่างเป็นทางการคือการใช้วิธีการทางคณิตศาสตร์เพื่อพิสูจน์ความถูกต้องหรือความไม่ถูกต้องตามข้อกำหนดหรือคุณสมบัติที่เป็นทางการอย่างใดอย่างหนึ่งหรือบางอย่าง

ความรู้สึกลึกลับอาจมาจากคำหลักที่เข้มงวดและเป็นนามธรรมสองคำในคำจำกัดความ - "ข้อกำหนดที่เป็นทางการ" และ "การพิสูจน์ด้วยวิธีการทางคณิตศาสตร์" ความจริงแล้ว การเปิดเผยชั้นความลับนี้ คุณจะพบกับแง่มุมที่น่าสนใจมากมายของการตรวจสอบอย่างเป็นทางการ

คำถามที่ฉันต้องการพูดคุยในบทความต่อไปนี้คือ: ในขั้นตอนนี้ เรื่องใดต่อไปนี้ที่สามารถตอบสนองจินตนาการของคุณเกี่ยวกับการตรวจสอบอย่างเป็นทางการได้ การตรวจสอบอย่างเป็นทางการสามารถจับได้ว่าเป็นเทคโนโลยีในพื้นที่ blockchain หรือไม่? ถ้าเป็นเช่นนั้นจะทำได้อย่างไร?

(ปล.: แนวคิดของ "ข้อกำหนดอย่างเป็นทางการ" ที่กล่าวถึงข้างต้นจะถูกกล่าวถึงด้านล่างด้วย)

ในการตอบคำถามข้างต้น ก่อนอื่นเรามาพิจารณาคำถามที่ง่ายกว่านี้ก่อน:

>ในขั้นตอนนี้ผู้คนใช้วิธีการที่เป็นทางการเพื่ออะไร?

มีเพียงสองคำตอบสำหรับคำถามนี้:

>1. หลีกเลี่ยงข้อผิดพลาด

>ชื่อระดับแรก

| หลีกเลี่ยงข้อผิดพลาด

การหลีกเลี่ยงข้อผิดพลาดคือการหลีกเลี่ยงการสูญเสียอย่างแท้จริง

เรามาสำรวจกันก่อนว่าพื้นที่ใดบ้างที่มีข้อผิดพลาดในการเขียนโปรแกรมเป็นศูนย์ การสูญเสียที่เกิดจากข้อผิดพลาดในการเขียนโปรแกรมนั้นนับไม่ถ้วนในด้านใด

ในความเป็นจริง วิธีการที่เป็นทางการได้รับความนิยมตั้งแต่การออกแบบฮาร์ดแวร์ ตัวอย่างที่โด่งดังคือ: หน่วยจุดลอยตัวของ CPU Pentium ของ Intel เกิดข้อผิดพลาด (ข้อผิดพลาด FDIV) และ CPU หลายหมื่นตัวต้องถูกรีไซเคิลและเปลี่ยนใหม่ ซึ่งก่อให้เกิดความสูญเสียอย่างมากต่อ Intel (475 ล้านเหรียญสหรัฐ)[1]

ตั้งแต่นั้นมา Intel ได้นำวิธีการที่เป็นทางการมาใช้อย่างกว้างขวางในการออกแบบชิป

ยักษ์ใหญ่ด้านฮาร์ดแวร์คอมพิวเตอร์เช่น IBM, AMD, NVIDIA และ CADENCE[2] ต่างก็ใช้วิธีทางการ...

ถ้าจะบอกว่าคุณสามารถเรียนรู้ภูมิปัญญามากมายผ่านคูน้ำ อันที่จริง มีคนลองผิดลองถูกในทุกสาขาอาชีพ และในโลกอุตสาหกรรมก็เช่นเดียวกัน ตัวอย่างเช่น ในปี 1996 การเปิดตัวจรวด Ariane 5 (Ariane 5) ครั้งแรกของ European Space Agency เนื่องจากคำสั่งที่ไม่ถูกต้องที่ส่งโดยระบบนำทางเฉื่อย (เลขทศนิยมแปลงเป็นจำนวนเต็มทำให้เกิดการล้น) จรวดจึงเปิดตัวเท่านั้น เป็นเวลา 37 วินาที จากนั้นมันก็เบี่ยงออกจากเส้นทางที่กำหนดไว้และชนในที่สุด ทุนวิจัยและพัฒนาจำนวนมหาศาลของ European Space Agency (8B $)[3] ลุกเป็นไฟ

หลังจากนั้นไม่นาน EADS ได้เริ่มใช้วิธีการที่เป็นทางการเพื่อพัฒนารูปแบบการจัดตารางภารกิจสำหรับจรวด Ariane

องค์การบริหารการบินและอวกาศแห่งชาติ NASA และกระทรวงกลาโหมอังกฤษได้ออกมาตรฐานการออกแบบอย่างต่อเนื่องในช่วงทศวรรษที่ 1990 [4] โดยระบุถึงการใช้วิธีการที่เป็นทางการ ระบบควบคุมยานสำรวจดวงจันทร์ Yutu ในประเทศของฉันและยานอวกาศที่พัฒนาเองลำแรกในประเทศของฉันซึ่งฝังระบบปฏิบัติการตามเวลาจริง SpaceOS[5] ยังตรวจสอบความถูกต้องด้วยวิธีการที่เป็นทางการ

พัฒนาการของประวัติศาสตร์บอกเราว่าเงินเป็นแรงผลักดันแรกในการส่งเสริมการพัฒนาสังคม! ไม่มีใครสามารถที่จะถอนหายใจกับความสูญเสียครั้งใหญ่ที่เกิดจากข้อผิดพลาดของโปรแกรม

หากสองเรื่องข้างต้นฟังดูหนักเกินไป ลองมาดูภาพต่อไปนี้:

รูปด้านบนแสดงการกระจายโครงการรถไฟใต้ดินทั่วโลกที่พัฒนาโดยใช้วิธีการที่เป็นทางการ [6]

จะเห็นได้ว่าเริ่มจากระบบอาณัติสัญญาณของรถไฟใต้ดินปารีส วิธีการที่เป็นทางการได้ถูกนำมาใช้อย่างแพร่หลายในการพัฒนาระบบรถไฟใต้ดินในประเทศใหญ่ๆ ในอเมริกาเหนือ ยุโรป เอเชีย และบางประเทศในอเมริกาใต้ นี่อาจเป็นเหตุผลว่าทำไมเราแทบไม่เคยได้ยินเกี่ยวกับความสูญเสียและภัยพิบัติครั้งใหญ่เนื่องจากความล้มเหลวของระบบรถไฟใต้ดิน

ย้ำอีกครั้งว่าเงินเป็นกำลังหลักในการผลิต

ขณะนี้การมีส่วนร่วมของวิธีการที่เป็นทางการในการรับรองการเดินทางทุกวันได้รับการยอมรับอย่างกว้างขวาง ในด้านของสินทรัพย์ดิจิทัลที่พัฒนาบนพื้นฐานของเทคโนโลยีบล็อกเชน เทคโนโลยีการตรวจสอบอย่างเป็นทางการสามารถใช้เพื่อรับรองความปลอดภัยของสัญญาอัจฉริยะ ซึ่งจะเป็นการปกป้องทรัพย์สิน แนวคิดของ ​​การรักษาความปลอดภัยจะสมเหตุสมผลและเร่งด่วน

ฉันควรทำอย่างไรดี? นี่คือคำแนะนำสั้น ๆ

ก่อนอื่น จำเป็นต้องแนะนำแนวคิดของ "ข้อมูลจำเพาะที่เป็นทางการ"

ข้อกำหนดอย่างเป็นทางการ (ข้อกำหนดที่เป็นทางการ) หมายถึงการดำเนินการอย่างเข้มงวดและครอบคลุมของลักษณะการทำงานที่คาดหวังของระบบ (เช่น การโอนโทเค็น S จำนวนหนึ่งจากบัญชี A ไปยังบัญชี B) และคุณสมบัติ (เช่น การโอนจะไม่ทำให้เกิดการล้นของบัญชี B ) ผ่านภาษาคณิตศาสตร์ ความหมาย ข้อกำหนดที่เป็นทางการมักจะกำหนดความถูกต้องและความปลอดภัยของระบบ

ด้วยข้อมูลจำเพาะที่เป็นทางการของระบบ เราสามารถออกแบบและใช้งานระบบซ้ำๆ โดยเริ่มจากข้อมูลจำเพาะ ในแต่ละขั้นตอนของการวนซ้ำ เราสามารถทำให้แน่ใจได้อย่างเคร่งครัดทางคณิตศาสตร์ว่าระบบที่เกิดจากการวนซ้ำนั้นสอดคล้องกับข้อกำหนดหรือระบบก่อนการวนซ้ำด้วยวิธีการต่างๆ รวมถึงการปรับแต่ง การสังเคราะห์ และการพิสูจน์อย่างเป็นทางการ

นอกเหนือจากการออกแบบและนำระบบไปใช้จากข้อกำหนดที่เป็นทางการแล้ว เรายังสามารถใช้ชุดวิธีการต่างๆ รวมถึงการดำเนินการเชิงสัญลักษณ์ การตรวจสอบแบบจำลอง และการพิสูจน์อย่างเป็นทางการเพื่อตรวจสอบว่าการออกแบบที่มีอยู่และการนำไปใช้นั้นสอดคล้องกับข้อกำหนดนี้

ฟังดูยิ่งใหญ่ใช่มั้ย

ตัวอย่างเช่น สำหรับโปรแกรมสัญญาอัจฉริยะ เราสามารถเริ่มต้นจากอินพุตที่เป็นไปได้ทั้งหมด (เช่น การรวมกันของพารามิเตอร์ฟังก์ชัน) และสถานะเริ่มต้น (เช่น การรวมกันของค่าเริ่มต้นของตัวแปรสถานะ) ตามความหมายของแต่ละคำสั่ง ทีละประโยค อนุมานสถานะสิ้นสุดที่เป็นไปได้ทั้งหมดของโปรแกรม (เช่น ค่าของตัวแปรสถานะและบันทึกเหตุการณ์ที่สร้างขึ้นหลังจากการดำเนินการตามสัญญา) และตรวจสอบว่าการรวมกันของอินพุตทั้งหมด สถานะเริ่มต้น และสถานะสิ้นสุดของ สัญญาสอดคล้องกับข้อกำหนดที่เป็นทางการ เรื่องนี้ค่อนข้างคล้ายกับวิธีที่โคนันไขคดีทีละขั้นตอน อย่างไรก็ตาม คำจำกัดความทั้งหมดในที่นี้อธิบายด้วยภาษาทางคณิตศาสตร์ที่เคร่งครัด และรากศัพท์และการตรวจสอบก็มาจากรากศัพท์และการพิสูจน์ทางคณิตศาสตร์ที่เข้มงวดเช่นกัน ขึ้นอยู่กับความซับซ้อนของระบบที่จะตรวจสอบและข้อกำหนดที่เป็นทางการ การสืบเชื้อสายและการพิสูจน์สามารถสร้างด้วยตนเองหรือสร้างขึ้นโดยอัตโนมัติโดยเครื่องจักร

ชื่อระดับแรก

| ต่อต้านการโจมตี

การโจมตีของฝ่ายตรงข้ามเป็นอีกความรู้สึกหนึ่งของการหลีกเลี่ยงการสูญเสีย

เรื่องราวเริ่มต้นด้วยการโจมตีทางอิเล็กทรอนิกส์โดยกองทัพสหรัฐ ในฤดูร้อนปี 2558 แฮ็กเกอร์ได้รับคำสั่งให้ทำการโจมตีทางอิเล็กทรอนิกส์กับเฮลิคอปเตอร์ไร้คนขับ Little Bird ของกองทัพสหรัฐฯ และเข้าควบคุมโดรน อย่างไรก็ตาม เมื่อกระทรวงกลาโหมสหรัฐพัฒนาโปรแกรมควบคุมหลักของ UAV ขึ้นใหม่ แฮ็กเกอร์ใช้วิธีโจมตีทั้งหมดในโลกปัจจุบัน แต่ล้มเหลวในการเจาะระบบที่ติดตั้งใหม่ [7]

เทคโนโลยีชนิดใดที่ทำให้ Little Bird มีความสามารถในการป้องกันขั้นสุดยอด จึงบล็อกการโจมตีทั้งหมดได้ คำตอบคือ วิธีการตรวจสอบอย่างเป็นทางการ

วิธีการตรวจสอบอย่างเป็นทางการช่วยให้มั่นใจได้ว่าพฤติกรรมของโปรแกรมสอดคล้องกับความคาดหวังผ่านการพิสูจน์ทางคณิตศาสตร์ที่เข้มงวด แต่ความถูกต้องของโปรแกรมการตรวจสอบอย่างเป็นทางการนั้นต้องใช้แรงงานมาก ดังนั้นจึงไม่เหมือนกับเทคนิควัตถุประสงค์ทั่วไป เช่น การทดสอบโปรแกรม วิธีการตรวจสอบอย่างเป็นทางการมักจะใช้กับความปลอดภัยเท่านั้น โดเมนที่สำคัญ เช่น การตรวจสอบความถูกต้องของโปรแกรมสำหรับโดรน ยานอวกาศ ระบบปฏิบัติการ ฯลฯ

สิ่งที่ฉันต้องพูดถึงคือ Dirty Cow (CVE-2016-5195)[8] ซึ่งเป็นช่องโหว่เคอร์เนลของระบบปฏิบัติการ Linux ที่ร้ายแรงมากซึ่งถูกค้นพบในปี 2559 ผู้โจมตีสามารถใช้ช่องโหว่นี้เพื่อรับสิทธิพิเศษสูงสุดของระบบ เพื่อให้ทั้งระบบ สามารถใช้ประโยชน์จากระบบได้ในสภาพการใช้งาน

ชื่อระดับแรก

| ฟิลด์บล็อคเชนที่สำคัญต่อความปลอดภัย

เช่นเดียวกันในด้านบล็อกเชน ในแง่หนึ่ง ความผิดพลาดเล็กน้อยอาจนำไปสู่ความสูญเสียครั้งใหญ่ ในทางกลับกัน ผลประโยชน์ทางเศรษฐกิจมหาศาลก็สามารถดึงดูดผู้โจมตีจำนวนมากได้เช่นกัน

ในกรณีการแฮ็ก Ethereum ครั้งใหญ่ครั้งแรก DAO ผู้โจมตีได้ขโมย Ethereum มูลค่า 55 ล้านดอลลาร์สหรัฐในขณะนั้น ซึ่งนำไปสู่การ Hard Fork Ethereum[11] หลังจากนั้น การโจมตีที่เกี่ยวข้องกับ Ethereum Smart Contract ก็ดำเนินต่อไป—เช่น ในเดือนพฤศจิกายน 2017 กระเป๋าเงิน Ethereum Parity ถูกแฮ็ก ทำให้ผู้ใช้สูญเสียทรัพย์สินดิจิทัลมูลค่าประมาณ 150 ล้านดอลลาร์ [11]

ตามสถิติจาก Ambi Labs ในช่วงครึ่งแรกของปี 2018 เพียงปีเดียว มีการขโมยสินทรัพย์ดิจิทัลประมาณ 1.1 พันล้านดอลลาร์ และช่องโหว่ที่เกี่ยวข้องกับระบบบล็อกเชน (เช่น ช่องโหว่สัญญาอัจฉริยะใน Ethereum) และระบบนิเวศโดยรอบสินทรัพย์ดิจิทัล ปัญหาด้านความปลอดภัย (เช่น เนื่องจากการขโมยการแลกเปลี่ยนแบบรวมศูนย์หลายรายการ) กำลังเกิดขึ้นในกระแสที่ไม่สิ้นสุด

ในปัจจุบัน ช่องโหว่ที่เกี่ยวข้องในระบบบล็อกเชนและปัญหาด้านความปลอดภัยของระบบนิเวศของสินทรัพย์ดิจิทัลนั้นเกี่ยวข้องกับการออกแบบและการใช้งานโปรแกรมที่เกี่ยวข้องในท้ายที่สุด ก่อนวิธีการที่เป็นทางการจะพบปัญหาดังกล่าวจากการทดสอบโปรแกรมเป็นส่วนใหญ่

ในช่วงแรก ๆ เมื่อการตรวจสอบอย่างเป็นทางการเข้าสู่สนามบล็อกเชน Yoichi Hirai จากชุมชน Ethereum ได้สร้างแบบจำลอง EVM เครื่องเสมือนสัญญาอัจฉริยะของ Ethereum อย่างเป็นทางการ นอกจากนี้ ทีมงานจากมหาวิทยาลัย UIUC ยังสร้างแบบจำลองและตรวจสอบ EVM อย่างเป็นทางการอีกด้วย [12] EVM เป็นแกนหลักของสัญญาอัจฉริยะของ Ethereum ซึ่งเกี่ยวข้องกับความปลอดภัยของ Ethereum และเกี่ยวข้องกับประเด็นสำคัญๆ เช่น การปกป้องทรัพย์สินดิจิทัลซึ่งได้รับความสนใจอย่างกว้างขวางจากชุมชน

นอกจากนี้ โครงการ MakerDAO ยังเปิดตัวแอปพลิเคชั่นกระจายอำนาจ (DApp) ที่ผ่านการตรวจสอบอย่างเป็นทางการเป็นครั้งแรก [13] MakerDAO เป็นแพลตฟอร์มสัญญาอัจฉริยะที่ใช้ Ethereum ซึ่งให้บริการ Stablecoins สินเชื่อค้ำประกัน และฟังก์ชั่นการกำกับดูแลชุมชนแบบกระจายอำนาจ เพื่อรับประกันความปลอดภัยของสัญญาอัจฉริยะที่ปรับใช้ ทีมงาน MakerDAO ได้ตรวจสอบรหัสสัญญาของสัญญากลไกหลักของเงินกู้จำนอง (CDP) ผ่าน K-Framewok ซึ่งแสดงให้เห็นว่าโปรแกรมสัญญาอัจฉริยะสามารถต้านทานการโจมตีของแฮ็กเกอร์ได้อย่างสมบูรณ์

Ambi Labs ยังได้ทำงานมากมายในการตรวจสอบ Ethereum smart contract อย่างเป็นทางการ เสนอกรอบการตรวจสอบอย่างเป็นทางการสำหรับ smart contracts และพิสูจน์สัญญา Token ทั่วไปภายในกรอบนี้ เช่น ERC20, ERC721 เป็นต้น (รวมถึงฟังก์ชันทั่วไปเช่น เป็นการโอน จำนวนโทเค็นทั้งหมด เป็นต้น) สัญญาอัจฉริยะที่ได้รับการพิสูจน์ทางคณิตศาสตร์เหล่านี้สามารถใช้ได้โดยตรงโดยไม่ต้องกังวลเกี่ยวกับปัญหาด้านความปลอดภัย ซอร์สโค้ดสัญญาและกระบวนการพิสูจน์เหล่านี้ได้สนับสนุนชุมชนในรูปแบบของโอเพ่นซอร์ส [14]

ชื่อระดับแรก

https://github.com/sec-bit/tokenlibs-with-proofs

| สรุป

คนส่วนใหญ่คิดว่าวิธีการตรวจสอบอย่างเป็นทางการนั้นกินลึกไม่ได้ เหตุผลคือ วิธีการตรวจสอบอย่างเป็นทางการไม่ใช่เทคโนโลยีทั่วไปแต่เป็นเทคโนโลยีเฉพาะที่ต้องใช้ร่วมกับภาคสนามเพื่อให้เห็นคุณค่าของมัน ในด้านบล็อกเชน ไม่ว่าวิธีการที่เป็นทางการจะดีหรือต้องมีก็เป็นสิ่งที่แยกออกจากลักษณะของโครงการไม่ได้เช่นกัน

ขณะที่การสำรวจเทคโนโลยีบล็อกเชนและแอปพลิเคชันโครงการยังคงลึกซึ้งยิ่งขึ้น ความต้องการของฝ่ายโครงการในการหลีกเลี่ยงข้อผิดพลาด ต่อต้านการโจมตีของแฮ็กเกอร์ และหลีกเลี่ยงการสูญเสียทรัพย์สินมีมากขึ้นเรื่อย ๆ

ชื่อระดับแรก

เขียนไว้ตอนท้าย | คุณรู้เรื่องความยุ่งเหยิงระหว่าง Verification และ Testing มากแค่ไหน?

สุดท้าย เรามาพูดถึงความสัมพันธ์ระหว่างการยืนยันอย่างเป็นทางการและการทดสอบ

"การทดสอบโปรแกรมสามารถพิสูจน์ได้ว่ามีข้อผิดพลาดอยู่จริง แต่ไม่สามารถพิสูจน์ได้ว่าไม่มีข้อผิดพลาด" Edsger Dijkstra (ผู้ชนะรางวัล Turing Award ในปี 1972 และผู้เสนอแนวคิดหลักของวิธีการอย่างเป็นทางการ) ให้ความเห็นในลักษณะนี้

ในทางปฏิบัติ โดยเฉพาะอย่างยิ่งในสถานการณ์ที่โค้ดมีความซับซ้อนเพียงพอ ผลการตรวจสอบของการตรวจสอบอย่างเป็นทางการ (Verification) และวิธีการทดสอบโปรแกรม (Testing) จะแตกต่างกันราวกับก้อนเมฆและโคลน

ตัวอย่างเช่น ในปี 2009 นักวิทยาศาสตร์ในออสเตรเลียใช้วิธีการที่เป็นทางการในการตรวจสอบการทำงานที่สมบูรณ์ของ seL4 microkernel ของระบบปฏิบัติการระดับอุตสาหกรรม [15] วิธีการตรวจสอบนั้นดำเนินการในสองวิธี: การตรวจสอบอย่างเป็นทางการและการทดสอบโปรแกรม ผลลัพธ์ของการตรวจสอบคือ: พบข้อบกพร่องมากกว่า 460 รายการโดยวิธีการที่เป็นทางการ แต่พบข้อบกพร่องเพียง 16 รายการจากการทดสอบโปรแกรม

สิ่งที่น่าสนใจกว่านั้นก็คือ ในด้านการตรวจสอบอย่างเป็นทางการซึ่งทราบกันดีว่ามีค่าใช้จ่ายสูงในการตรวจสอบ ค่าใช้จ่ายในการตรวจสอบยืนยัน seL4 microkernel อย่างสมบูรณ์นั้นอยู่ที่ 6 ล้านดอลลาร์สหรัฐเท่านั้น ในขณะที่ค่าใช้จ่ายในการผ่านการรับรอง CC EAL6 โดยการทดสอบนั้นสูงถึง 87 ล้านดอลลาร์สหรัฐฯ [15 ]

จะเห็นได้ว่าการตรวจสอบอย่างเป็นทางการสามารถให้การรับประกันความปลอดภัยที่แข็งแกร่งยิ่งขึ้นสำหรับ seL4 microkernel ในราคาประหยัด

อ้างอิง

อ้างอิง

【1】History of Formal Verification at Intel

https://dac.com/blog/post/history-formal-verification-intel

[2] Wang Jian: พูดคุยเกี่ยวกับการตรวจสอบอย่างเป็นทางการ

http://chainb.com/?P=Cont&id=1957

【3】Modeling and Validation of a Software Architecture for the Ariane-5 Launcher

https://link.springer.com/chapter/10.1007/11768869_6

【4】Tenth NASA Formal Methods Symposium 

https://shemesh.larc.nasa.gov/NFM2018/

[5] ระบบปฏิบัติการ SpaceOS ในประเทศที่ใช้โดย Yutu คาดว่าจะได้รับเป็นเวอร์ชันสำหรับพลเรือนในอนาคต

http://blog.sina.com.cn/s/blog_ae55841d0101hemg.html

【6】Cimatti, A., Corvino, R., Lazzaro, A., Narasamdya, I., Rizzo, T., Roveri, M., Sanseviero, A. and Tchaltsev, A., 2012, July. Formal verification and validation of ERTMS industrial railway train spacing system. In International Conference on Computer Aided Verification (pp. 378-393). Springer, Berlin, Heidelberg.

【7】COMPUTER SCIENTISTS CLOSE IN ON PERFECT, HACK-PROOF CODE https://www.wired.com/2016/09/computer-scientists-close-perfect-hack-proof-code/

[8] ใช้ Dirty Cow เพื่อให้นักเทียบท่าหลบหนี

https://www.anquanke.com/post/id/84866

【9】CertiKOS: Yale develops world’s first hacker-resistant operating system

https://www.ibtimes.co.uk/certikos-yale-develops-worlds-first-hacker-resistant-operating-system-1591712

【10】Fengwei Xu, Ming Fu, Xinyu Feng, Xiaoran Zhang, Hui Zhang and Zhaohui Li. A Practical Verification Framework for Preemptive OS Kernels. Proc. 28th International Conference on Computer Aided Verification (CAV’16)

【11】การวิเคราะห์วิธีการโจมตีต่อ THE DAO จากมุมมองทางเทคนิค

https://www.8btc.com/article/93713

【12】kframework/evm-semantics

https://github.com/kframework/evm-semantics

【13】บริษัทร่วมทุนยักษ์ใหญ่ A16Z ลงทุนในโครงการสกุลเงินที่มั่นคง MakerDAO

https://www.jinse.com/bitcoin/246582.html

[14] การสร้างหลักฐานที่เป็นทางการเพื่อแก้ปัญหาความปลอดภัยของสัญญาอัจฉริยะ - สัญญาของคุณจำเป็นต้องได้รับการพิสูจน์อย่างเร่งด่วน

https://mp.weixin.qq.com/s/xUNKT8v9ikEYFnuMWzvXdg

【15】Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles (SOSP '09).