หัวหน้านักวิทยาศาสตร์ของ CertiK Vilhelm Sjöberg: การสร้างสัญญาอัจฉริยะและระบบนิเวศบล็อกเชนที่น่าเชื่อ

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

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

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

เมื่อวันที่ 5 กันยายน ที่การประชุม blockchain POD ซึ่งจัดโดย Odaily และร่วมจัดโดย 36Kr Group Strategy Vilhelm Sjöberg หัวหน้านักวิทยาศาสตร์ของ CertiK กล่าวสุนทรพจน์ในหัวข้อ "สู่การสร้างสัญญาอัจฉริยะที่น่าเชื่อถืออย่างเต็มที่และระบบนิเวศของบล็อกเชน"

ชื่อเรื่องรอง

ต่อไปนี้เป็นสำเนาของสุนทรพจน์โดย Vilhelm Sjöberg หัวหน้านักวิทยาศาสตร์ของ CertiK:

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

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

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

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

เคอร์เนลของโปรแกรมปฏิบัติการ CertiKOS ของเราแบ่งออกเป็นหลายชั้น และสามารถตรวจสอบโปรแกรมขนาดใหญ่และซับซ้อนได้ เนื่องจากเรากำลังจัดการกับฟังก์ชันที่ซับซ้อนทีละฟังก์ชัน

ภาพนี้แสดงให้เห็นว่าเราติดตั้งระบบปฏิบัติการ CertiKOS บนเครื่อง Landshark

เรายังร่วมมือกับผู้เชี่ยวชาญในแวดวงวิชาการมากมายและพวกเขาช่วยเราพัฒนาโครงการดังกล่าว ในปี 2015 ศาสตราจารย์ Gu Ronghui และศาสตราจารย์ Shao Zhong ได้เสนอแนวคิดของ "ข้อกำหนดเชิงลึก" และตรวจสอบความถูกต้อง ในปี 2559 เราได้ขายผลิตภัณฑ์และบริการพร้อมใช้นี้ให้กับธุรกิจต่างๆ แล้ว ในปี 2560 เราได้ขยาย CertiK เพื่อตรวจสอบสัญญาอัจฉริยะ ดังนั้นเราจึงสามารถทำการวิจัยเชิงวิชาการ และดำเนินการตรวจสอบอย่างเป็นทางการสำหรับบล็อกเชนได้

ต่อไป ให้ฉันแนะนำรายละเอียดเกี่ยวกับโครงการวิจัยต่อเนื่องที่เราดำเนินการ - DeepSEA ซึ่งเป็นภาษาการเขียนโปรแกรมสำหรับตรวจสอบสัญญาอัจฉริยะ

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

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

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

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

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

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