Yang Wenyu, Cheetah Blockchain Research Center: มีปัญหาหลักสามประการในการตรวจสอบสัญญาอัจฉริยะโดยอัตโนมัติ: อัตราบวกเท็
เมื่อวันที่ 5 กันยายน ที่การประชุม POD Conference Security Forum ซึ่งจัดโดย Odaily และร่วมจัดโดย 36Kr Group Strategy Yang Wenyu ผู้เชี่ยวชาญด้านความปลอดภัยจาก Cheetah Blockchain Research Center ได้กล่าวสุนทรพจน์ในหัวข้อ "Smart Contract Automated Audit Technology"
Yang Wenyu แนะนำสถานะปัจจุบันของการพัฒนาสัญญาอัจฉริยะ คนส่วนใหญ่คิดว่าบล็อกเชนอยู่ในช่วงฤดูหนาว แต่จากสถิติของ Cheetah Blockchain Research Center ในเดือนที่ผ่านมา จำนวนสัญญาอัจฉริยะใหม่อยู่ที่ 1,317 รายการต่อวัน ในบรรดาโครงการที่รวมอยู่ในศูนย์วิจัย โครงสร้างพื้นฐานบล็อกเชนคิดเป็น 9.38% เกมและ VR 4.44% การค้าและการค้าปลีก 3.6% และโซเชียลมีเดียและการสื่อสาร 3.4%
ในขณะที่จำนวนเพิ่มขึ้นเรื่อย ๆ สัญญาอัจฉริยะก็ประสบปัญหาด้านความปลอดภัยเช่นกัน ตั้งแต่ปี 2017 ถึงมิถุนายน 2018 ช่องโหว่ของสัญญาอัจฉริยะเกิดขึ้นบ่อยครั้ง ทำให้เกิดการสูญเสียทางการเงินจำนวนมาก และทำให้นักพัฒนาซอฟต์แวร์หรือผู้ใช้บล็อกเชนและแม้แต่สัญญาอัจฉริยะบางคนตั้งคำถามถึงความปลอดภัยของสัญญาอัจฉริยะ ซึ่งเป็นอุปสรรคต่อการพัฒนา Ethereum ในภายหลัง Ethereum การพัฒนาของ
นอกจากนี้ เมื่อ Fomo3D กำลังเติบโต สัญญาปลอมจำนวนมากก็ปรากฏขึ้นในวันที่สองเท่านั้น ผู้พัฒนาเกม Fomo3D เลียนแบบได้เปลี่ยนตรรกะของการเผยแพร่ที่ใช้งานอยู่ ทำให้เงินลงทุนส่วนใหญ่ไหลไปยังผู้พัฒนาสัญญาลอกเลียนแบบ ซึ่งเป็นอุปสรรคต่อการพัฒนา DApps
ในบริบทนี้ จะรับประกันความปลอดภัยของสัญญาอัจฉริยะจำนวนมากอย่างมีประสิทธิภาพได้อย่างไร Yang Wenyu เชื่อว่าวิธีที่ดีที่สุดคือการลดความซับซ้อนของการตรวจสอบด้วยตนเอง และใช้สัญญาอัจฉริยะในการตรวจสอบโดยอัตโนมัติ
โดยเฉพาะอย่างยิ่ง วิธีการตรวจสอบอัตโนมัติแบ่งออกเป็นสามประเภทหลัก:
ประการแรกคือการจับคู่รหัสคุณลักษณะ ซึ่งคือการแยกและสรุปรหัสที่เป็นอันตราย และสร้างโมดูลการจับคู่เพื่อตรวจหาซอร์สโค้ดที่จะตรวจพบ ข้อดีคือความเร็วที่รวดเร็วและการตอบสนองต่อช่องโหว่ใหม่อย่างรวดเร็ว แต่ข้อเสียคือขอบเขตการใช้งานที่จำกัดและอัตราการลบที่ผิดพลาดสูง
วิธีที่สองคือวิธีการตรวจสอบอัตโนมัติตามการตรวจสอบอย่างเป็นทางการ จัดทำขึ้นครั้งแรกโดย Hirai ในปี 2559 และปรับปรุงหลังจาก Grishchenko และ Hildenbrandt โดยใช้ F*framework และ K framework เพื่อแปลง EVM เป็นโมเดลที่เป็นทางการ รูปแบบเป็นกรอบการตรวจสอบที่เป็นทางการทั่วไปในฟิลด์การบินและอวกาศ ในขณะที่กรอบ K เป็นกรอบการแปลงความหมาย
วิธีสุดท้ายคือวิธีที่ใช้บ่อยที่สุดในปัจจุบัน โดยอิงตามการดำเนินการเชิงสัญลักษณ์และนามธรรมเชิงสัญลักษณ์เพื่อทำให้การตรวจสอบเป็นไปโดยอัตโนมัติ เมื่อวิเคราะห์สัญญาอัจฉริยะ EVM OPCODE สามารถสร้างขึ้นได้โดยการคอมไพล์ซอร์สโค้ด จากนั้นป้อนข้อมูลไปยังเครื่องมือวิเคราะห์อัตโนมัติ แปลงเป็น CFG แล้ววิเคราะห์โดยใช้สองวิธีนี้ ระบบทั่วไปคือระบบ Oyente และ Securify ซึ่งสามารถลดอัตราการเกิด False Positive และ False Negative ได้ แต่วิธีการวิเคราะห์นั้นยุ่งยากและใช้เวลานาน
อย่างไรก็ตาม Yang Wenyu ยังชี้ให้เห็นว่าวิธีการตรวจสอบอัตโนมัติในปัจจุบันนั้นยังไม่สมบูรณ์นัก และส่วนใหญ่ประสบปัญหาสำคัญสามประการ ได้แก่ อัตราการเตือนที่ผิดพลาดสูง ระดับการทำงานอัตโนมัติต่ำ การพึ่งพาการตรวจสอบรองด้วยตนเอง และเวลาการตรวจสอบที่ค่อนข้างนาน
ต่อไปนี้เป็นข้อความทั้งหมดของสุนทรพจน์ของ Yang Wenyu ขอให้สนุก:
ขอขอบคุณทุกท่าน รู้สึกเป็นเกียรติอย่างยิ่งที่ได้เข้าร่วมการประชุมในวันนี้ หัวข้อสุนทรพจน์ของฉันในวันนี้คือการวิเคราะห์เทคโนโลยีปัจจุบันของการตรวจจับความปลอดภัยระบบสัญญาอัตโนมัติอัจฉริยะ สุนทรพจน์ของฉันในวันนี้อาจแบ่งออกเป็นสองส่วน ส่วนแรก เราจะหารือเกี่ยวกับ ส่วนแรก มาดูสถานะปัจจุบันของการพัฒนาสัญญาอัจฉริยะบน Ethereum ส่วนที่สองขึ้นอยู่กับสถานะที่เป็นอยู่นี้และจากนั้นจะอธิบายรายละเอียดเกี่ยวกับวิธีการบางอย่างที่เกี่ยวข้องกับสัญญาอัจฉริยะอัตโนมัติ
ก่อนอื่น เรามาดูสถานะปัจจุบันของการพัฒนาสัญญาอัจฉริยะ จากแพลตฟอร์มของเรา เราสามารถทราบได้ว่าในเดือนที่ผ่านมา จำนวนสัญญาอัจฉริยะเพิ่มขึ้นอย่างต่อเนื่องในอัตราการเติบโตเฉลี่ย 1317 ต่อวัน ซึ่งอาจตรงกับความเข้าใจของเรา ตอนนี้ blockchain อยู่ในช่วงฤดูหนาว ดังนั้นอัตราการเติบโตจึงค่อนข้างคงที่ ประการที่สอง เราใช้วิธี NLT บางอย่างเพื่อแบ่งเขตข้อมูลของสัญญาอัจฉริยะ ขณะนี้ สัญญาอัจฉริยะถูกนำมาใช้อย่างแพร่หลายในโครงสร้างพื้นฐาน การค้าปลีก เกม สื่อสังคมออนไลน์ และการสื่อสาร ยกเว้นบางพื้นที่ที่ละเอียดอ่อน นี่คือสถานะที่เป็นอยู่ของสัญญาอัจฉริยะ สถานะความปลอดภัยของสัญญาอัจฉริยะตอนนี้เป็นอย่างไร บางทีแขกรับเชิญทั้งสองรายอาจอธิบายอย่างละเอียดแล้ว จากปี 2560 ถึงมิถุนายน 2561 ช่องโหว่สัญญาอัจฉริยะประเภทนี้เกิดขึ้นบ่อยครั้ง แต่ละครั้ง นำมาซึ่งความสูญเสียทางการเงินจำนวนมาก และยังทำให้นักพัฒนาบางคนหรือผู้ใช้ blockchain และแม้แต่สัญญาอัจฉริยะบางคนมีข้อสงสัยอย่างมากเกี่ยวกับความปลอดภัยของสัญญาอัจฉริยะ ซึ่งเป็นอุปสรรคต่อการพัฒนา Ethereum
นอกจากนี้เรายังเห็นได้ว่าแขกพูดถึง Fomo3D ในตอนนี้ นอกเหนือจากการรักษาความปลอดภัยสัญญาอัจฉริยะขั้นพื้นฐานแล้วความปลอดภัยยังได้รับความสนใจอย่างมาก เมื่อ Fomo3D ได้รับความนิยมสัญญาอัจฉริยะจำนวนมากก็ปรากฏขึ้นในวินาทีที่สอง วัน ในเกมประเภทนี้ผู้พัฒนาเปลี่ยนตรรกะของการจัดสรรที่ใช้งานจริงดังนั้นในกระบวนการเล่นเกมรังผึ้งเงินส่วนใหญ่ที่ลงทุนจะไหลไปยังผู้พัฒนาสัญญาเลียนแบบซึ่งมีส่วนช่วยในการพัฒนา ปพ.ทำให้เกิดอุปสรรค
ตอนนี้เรากำลังประสบปัญหาเกี่ยวกับวิธีการรับประกันความปลอดภัยของสัญญาอัจฉริยะขนาดใหญ่อย่างมีประสิทธิภาพ ซึ่งเป็นปัญหาที่เราจะหารือในวันนี้ และส่วนที่สองที่ฉันต้องการแบ่งปันกับคุณเกี่ยวกับการพัฒนาเทคโนโลยีการตรวจสอบระบบอัตโนมัติของสัญญาอัจฉริยะในปัจจุบัน
เมื่อมองย้อนกลับไป ณ เวลา 12.00 น. ของเมื่อวาน มีสัญญาอัจฉริยะทั้งหมด 1.93 ล้านรายการใน Ethereum และอัตราการเติบโตรายวันก็เพิ่มขึ้นเรื่อย ๆ ตอนนี้วิธีการตรวจสอบรวมถึงการตรวจสอบด้วยตนเองและการตรวจสอบอัตโนมัติ ในบรรดาสัญญาอัจฉริยะขนาดใหญ่ วิธีที่ดีที่สุดของเราคือการลดความซับซ้อนของการตรวจสอบด้วยตนเอง เพื่อให้สามารถทำได้มากขึ้นผ่านการตรวจสอบอัตโนมัติ เราแบ่งการตรวจสอบอัตโนมัติออกเป็นสามส่วน ประการแรก ประเภทแรกคือการจับคู่รหัสคุณสมบัติ ประเภทที่สองคือวิธีการตรวจสอบย่อยตามหน้าที่ตามการตรวจสอบสถานการณ์ และประเภทสุดท้ายคือการตรวจสอบอัตโนมัติตามการดำเนินการเชิงสัญลักษณ์และนามธรรมเชิงสัญลักษณ์
ดูที่การจับคู่รหัสคุณสมบัติก่อน สามารถเข้าใจได้อย่างชัดเจนจากชื่อที่แยกและสรุปรหัสที่เป็นอันตราย เราเป็นการจับคู่ความหมายที่ตรงกับรหัสต้นฉบับแบบคงที่ ข้อดีของวิธีการตรวจสอบนั้นชัดเจนเช่นความเร็วมาก อย่างรวดเร็วเนื่องจาก ทำการจับคู่สตริงในซอร์สโค้ด และรายการที่สองสามารถค้นหาช่องโหว่ใหม่ได้อย่างรวดเร็ว หากมีช่องโหว่ใหม่ในการตรวจสอบ เราสามารถส่งรูปแบบการจับคู่ใหม่ได้อย่างรวดเร็ว มีจุดบกพร่องอย่างไร มาดูกันอีกที เราเข้าใจว่าบล็อกเชนปัจจุบันควรเปิดกว้างและโปร่งใส แต่สถานการณ์จริงไม่ใช่แบบนี้ เราคงสร้างสถิติไว้ อัตราการเปิดรหัสปัจจุบันคิดเป็น 48.62% เท่านั้น , กล่าวคือบน Ethereum กว่าครึ่งของสัญญาไม่ใช่โอเพ่นซอร์ส มีเพียงโค้ดเท่านั้นที่ถูกเปิดเผย แขกรับเชิญกล่าวว่าพวกเขาใช้ความพยายามอย่างมากในการสร้างโค้ด ข้อจำกัดนี้นำไปสู่ขอบเขตการใช้งาน วิธีการนี้จำกัดวิธีการตรวจสอบแบบคงที่แบบดั้งเดิม เช่น การตรวจจับแอป จะเรียกใช้ฟังก์ชันเฉพาะบางอย่างในไลบรารีเพื่อตรวจสอบฟังก์ชันและฟีเจอร์บางอย่างในสัญญาอัจฉริยะจะแปรผันมากกว่า ดังนั้นอัตราช่องโหว่จึงค่อนข้างสูง
วิธีที่สอง เรามาพูดถึงการตรวจสอบอัตโนมัติยอดนิยมตามการยืนยันอย่างเป็นทางการ Hirai จัดทำการตรวจสอบการยืนยันอย่างเป็นทางการเป็นครั้งแรกในปี 2559 การพิสูจน์เชิงโต้ตอบเชิงลอจิคัล ผ่าน Isabelde Lem-Language->Formal-model ผ่านการตรวจสอบแบบจำลองอย่างเป็นทางการ เพื่อ ตัดสินว่ามีปัญหาใน code logic หรือไม่ สองงานสุดท้ายของงานนี้ได้ปฏิรูปรูปแบบที่เป็นทางการเพิ่มเติม พวกเขาเลิกใช้ Lem-language ซึ่งเป็นวิธีการแปลงที่ค่อนข้างไม่มีประสิทธิภาพ พวกเขาใช้ F*framework และ K framework เพื่อแปลง EVM เป็น รูปแบบที่เป็นทางการ และรูปแบบที่เป็นทางการอาจเป็นกรอบที่มักจะทำการตรวจสอบอย่างเป็นทางการในด้านการบินและอวกาศ ในขณะที่กรอบ K เป็นกรอบการเปลี่ยนแปลงความหมาย งานวิจัยทางเทคนิคที่เป็นตัวแทนทั้งสองนี้ ถ้าคุณต้องการมีความเข้าใจที่ลึกซึ้งยิ่งขึ้น คุณสามารถอ้างถึง เอกสารต่อไปนี้

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

หลังจากการสร้าง CFG ตอนนี้มีวิธีการวิเคราะห์สองวิธี ประเภทแรกคือการตรวจสอบตามการใช้สัญลักษณ์ ประเภทนี้เป็นตัวแทนมากขึ้น ทุกคนคุ้นเคยกับ Mythril, Oyente และ Maian วิธีวิเคราะห์นามธรรมเชิงสัญลักษณ์ที่เปิดเผยต่อสาธารณะคือ Securify วันนี้ฉันจะพูดถึงสถาปัตยกรรมเฉพาะและวิธีการใช้งานของทั้งสองระบบ Oyente และ Securify เป็นหลัก อันดับแรก มาดูที่ Oyente เราจะเห็นตรรกะของ Oyente จากด้านซ้าย ใน CFG หลังแอปพลิเคชัน ตัวแรกคือ explorer ซึ่งจะตรวจสอบแต่ละกระบวนการในรหัสและทำการตรวจสอบอย่างเป็นทางการ เช่นนี้ เราจะตรวจสอบว่าเรามี X หรือไม่ เพื่อให้ X ไม่เพียงเป็นไปตามเงื่อนไขของ C1, C2 และ C3 เท่านั้น ในตอนนี้ เราสามารถกำหนด ไม่ว่าจะเป็นสถานะไม่ใช่หรือใช่ เพื่อตรวจสอบการไหลของตรรกะทั้งหมด การวิเคราะห์หลักที่สองเป็นส่วนหลักที่สุดของ Oyente โดยจะแปลงเส้นทาง explorer ที่เพิ่งส่งออกและดำเนินการตรวจสอบช่องโหว่บางส่วนเท่านั้น ปัจจุบัน ให้บริการเฉพาะ TOD, Timestamp dependency และ Mishandled ข้อยกเว้น การยืนยันทั้งสามนี้ ในท้ายที่สุด นี่ ระบบสามารถรับประกันอัตราการเกิด False Positive และ False Negative ได้ โดยจะใช้ตัวตรวจสอบโอเพ่นซอร์สของ Microsoft เพื่อสรุปสถาปัตยกรรมโดยรวม ในกระบวนการที่เราเพิ่งอธิบายไป คุณควรเข้าใจด้วยว่า CFG to Explorer การตรวจสอบ บางครั้งเราต้องวนรอบเขา และแต่ละครั้งเป็นการตรวจสอบ ดังนั้นวิธีการวิเคราะห์นี้จึงใช้เวลานานเป็นพิเศษและอาจไม่ประสบความสำเร็จ นี่คือจุดที่ Oyente มีปัญหาใหญ่ในปัจจุบัน

บนพื้นฐานของปัญหานี้ เช่น Securify พวกเขาให้วิธีการอื่น พวกเขาเชื่อว่ารหัสสัญญาปัจจุบันนั้นง่ายเป็นพิเศษในการแยกส่วน ซึ่งแตกต่างจากรหัสแบบดั้งเดิม การเชื่อมต่อนั้นสูงเป็นพิเศษ เช่น รหัสสัญญาบางรูปแบบที่ค่อนข้างตายตัว เรา ไม่จำเป็นต้องดำเนินการตรวจสอบ Logic ของสัญญาทั้งหมด เราวิเคราะห์แต่ละโมดูลของการแยกส่วนสัญญาเพื่อปรับปรุงระดับของการทำงานอัตโนมัติ ภาพด้านซ้ายแสดงกระบวนการตรวจสอบทั้งหมด รหัสไบต์ของสัญญาจะถูกส่งผ่านภาษาโดเมน จากนั้นมี เป็นโมดูลการตรวจสอบ โดยเฉพาะอย่างยิ่งเช่นการจับคู่รูปแบบที่กล่าวถึงก่อนหน้านี้ ซึ่งจะแปลงช่องโหว่บางส่วนเป็นกรอบการจับคู่รูปแบบภาษาการตรวจสอบ และตรวจสอบว่าความหมายเข้ากันได้กับสิ่งนี้หรือไม่ ท้ายสุดจะมีการให้รายงานด้วยวิธีการตรวจสอบอัตโนมัตินี้ผู้จัดการที่สามารถส่งออกกระเป๋าสตางค์ได้ในที่สุดสามารถแก้ไขได้
ประเด็นที่เจาะจงกว่านั้นก็คือวิธีการวิเคราะห์เชิงความหมาย อันที่จริง การวิเคราะห์โค้ด explorer นี้มาจากสองมิติ มิติแรกคือลอจิก และสองคือข้อมูล เมธอดเชิงตรรกะกำหนดตรรกะสองประเภท ประเภทแรกเรียกว่า MayFollow และอันที่สองเรียกว่า MustFollow MayFollow หมายความว่า L2 ต้องมีพาธตามหลัง L1 และ MustFollow หมายความว่าทุกพาธของ L2 ต้องตามด้วย L1 ความแตกต่างทั้งสองนี้กำหนดกรอบตรรกะทั้งหมด
แบบที่สอง คือ ข้อมูล วิธีกำหนดการเปลี่ยนแปลงข้อมูลในสัญญามี 3 แบบ แบบแรกคือ MayDepOn มีสองปัจจัย ปัจจัยหนึ่งเรียกว่า Y และอีกปัจจัยหนึ่งเรียกว่า T เมื่อ T เปลี่ยนแปลง Y อาจเปลี่ยนแปลงหรือไม่ก็ได้ ประการที่สองคือ Eq นั่นคือ Y ถูกกำหนดโดย T อันที่สามคือ DetBy, Y และ T อยู่ในการติดต่อแบบหนึ่งต่อหนึ่ง ตราบใดที่ T เปลี่ยนเป็น Y มันจะเปลี่ยนแน่นอน นี่เป็นวิธีจินตนาการที่ชัดเจนกว่า อันที่จริง Maydepon ก็เหมือนกับตัวแปร T ของเราคือ เวลา, ในช่วงระยะเวลาหนึ่ง, Y อาจเป็นค่า, T เปลี่ยนแปลง, Y อาจไม่เปลี่ยนแปลง, ที่สามคือความสัมพันธ์แบบหนึ่งต่อหนึ่ง, เหมือนกับที่เราคำนวณแฮช, ตราบใดที่คุณเปลี่ยน T, Y จะต้องเปลี่ยน, ผ่านสองมิติของลอจิกและข้อมูล พวกเขาทำการตรวจสอบ และโมดูลการตรวจสอบขั้นสุดท้ายมีภาษาการตรวจสอบช่องโหว่ของสัญญาอัจฉริยะประมาณ 6 หรือ 7 ภาษา ภาษานี้เขียนขึ้นในปลั๊กอิน และนักพัฒนาด้านความปลอดภัยรายอื่น ๆ สามารถเพิ่มการยืนยันได้ต่อไป ภาษาแห่งความเปราะบาง .
ในตอนท้าย เมื่อเราประเมินการตรวจสอบอัตโนมัติ เราจำเป็นต้องจัดเตรียมเรื่องนี้จากระดับของการทำงานอัตโนมัติ อัตราของผลบวกปลอม และอัตราของผลบวกลวง ขณะนี้เราทราบแล้วว่าข้อมูลสามารถถูกผูกไว้ได้ และข้อมูลที่ตรวจพบ ยังคงต้องได้รับการยืนยันด้วยตนเองอีกครั้ง งานนี้ยุ่งยากมาก และอัตรา False Positive สามารถลดลงได้ด้วยวิธีนี้ วิธีการตรวจสอบแบบอัตโนมัติสองวิธีนี้สำหรับการดำเนินการเชิงสัญลักษณ์และนามธรรมเชิงสัญลักษณ์

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



