นักวิจัยจาก สถาบันแห่งรัฐเพื่อการวิจัยด้านสารสนเทศและระบบอัตโนมัติ (อินเรีย), Microsoft Research และ Carnegie Mellon University นำเสนอ รุ่นทดลองใช้ครั้งแรกของ ไลบรารีการเข้ารหัสลับของ EverCrypt พัฒนาขึ้นภายใต้กรอบของโครงการ Everest และใช้วิธีการทางคณิตศาสตร์ในการตรวจสอบความน่าเชื่อถืออย่างเป็นทางการ
สำหรับความสามารถและประสิทธิภาพ EverCrypt อยู่ใกล้กับไลบรารี crypto ที่มีอยู่มาก (OpenSSL) แต่ที่แตกต่างจากพวกเขาคือการรับประกันความน่าเชื่อถือและความปลอดภัยเพิ่มเติม
เช่น กระบวนการตรวจสอบจะลดลงไปจนถึงการกำหนดคุณสมบัติโดยละเอียด ที่อธิบายพฤติกรรมทั้งหมดของโปรแกรม และการพิสูจน์ทางคณิตศาสตร์ว่ารหัสที่เขียนขึ้น ตรงตามข้อกำหนดที่เตรียมไว้
ไม่เหมือนกับวิธีการควบคุมคุณภาพตามหลักฐาน การตรวจสอบให้การรับประกันที่เชื่อถือได้ ว่าโปรแกรมจะทำงานตามที่นักพัฒนาตั้งใจไว้เท่านั้นและไม่มีข้อผิดพลาดเฉพาะบางคลาส
ตัวอย่างเช่นการปฏิบัติตามข้อกำหนด ช่วยให้มั่นใจได้ว่าปลอดภัยในการทำงานกับหน่วยความจำและไม่มีข้อผิดพลาดที่ทำให้เกิดบัฟเฟอร์ล้นเพื่อหักล้างพอยน์เตอร์เพื่อเข้าถึงพื้นที่หน่วยความจำที่ว่างอยู่แล้วหรือเพื่อปลดปล่อยบล็อกหน่วยความจำสองเท่า
EverCrypt คืออะไร?
เอเวอร์คริปต์ ให้การตรวจสอบประเภทและค่าที่มีประสิทธิภาพ- ส่วนประกอบจะไม่ส่งผ่านพารามิเตอร์ไปยังส่วนประกอบอื่น ๆ ที่ไม่เป็นไปตามข้อกำหนดและจะไม่สามารถเข้าถึงสถานะภายในของส่วนประกอบอื่น ๆ ได้
พฤติกรรมอินพุต / เอาต์พุต สอดคล้องกับการกระทำของฟังก์ชันคณิตศาสตร์อย่างง่ายซึ่งกำหนดไว้ในมาตรฐานการเข้ารหัส
เพื่อป้องกันการโจมตี ในช่องของบุคคลที่สาม พฤติกรรมระหว่างการคำนวณ (ตัวอย่างเช่นระยะเวลาของการดำเนินการหรือการมีอยู่ของการเข้าถึงหน่วยความจำบางอย่าง) ไม่ได้ขึ้นอยู่กับข้อมูลลับที่ประมวลผล
รหัสโครงการ เขียนด้วยภาษาที่ใช้งานได้ F * (F ดาว) , ซึ่งจัดเตรียมระบบประเภทขึ้นอยู่กับและการปรับแต่งซึ่งอนุญาตให้สร้างข้อกำหนดที่แน่นอน (แบบจำลองทางคณิตศาสตร์) สำหรับโปรแกรมและเพื่อรับประกันความถูกต้องและไม่มีข้อผิดพลาดในการใช้งานโดยใช้สูตร SMT และเครื่องมือทดสอบเสริม
รหัสใน F * เผยแพร่ภายใต้ลิขสิทธิ์ Apache 2.0 และโมดูลสุดท้ายใน C และแอสเซมเบลอร์ภายใต้ใบอนุญาต MIT
ขึ้นอยู่กับรหัสอ้างอิง F * แอสเซมเบลอร์, C, OCaml, JavaScript ถูกสร้างขึ้น และรหัสการประกอบเว็บ
บางส่วนของรหัส ที่เตรียมไว้ โดยโปรเจ็กต์ถูกใช้แล้วใน Firefox เคอร์เนลของ Windows บล็อกเชนของ Tezos และ VPN Wireguard
ส่วนประกอบ EverCrypt
ในสาระสำคัญ, EverCrypt รวมสองโครงการที่แตกต่างกันก่อนหน้านี้จาก HACL * และ Valeจัดเตรียม API แบบรวมที่อ้างอิงจาก API เหล่านี้และทำให้เหมาะสำหรับใช้ในโครงการจริง
HACL * เขียนด้วยภาษาต่ำ* และเป้าหมายของมันคือการจัดเตรียมการเข้ารหัสแบบดั้งเดิมสำหรับใช้ในโปรแกรม C ที่ พวกเขาใช้ API สไตล์ libsodium และ NaCL
โครงการ Vale พัฒนาภาษาเฉพาะ โดเมนเพื่อสร้างการยืนยันในแอสเซมเบลอร์
โค้ด HACL * ประมาณ 110 บรรทัดในภาษาต่ำ * และโค้ด 25 บรรทัดสำหรับ Vale ถูกรวมเข้าด้วยกัน และมีการเขียนโค้ดประมาณ 70 บรรทัดในภาษาสากล F * ซึ่งกำลังได้รับการพัฒนาเช่นกัน ซึ่งเป็นส่วนหนึ่งของโครงการ Everest
เวอร์ชันแรกของไลบรารี EverCrypt คุณสมบัติการใช้งานที่ได้รับการยืนยัน อัลกอริทึมการเข้ารหัสต่อไปนี้ เสนอในเวอร์ชัน C หรือแอสเซมเบลอร์ (เมื่อใช้ไฟล์.
สิ่งต่อไปนี้โดดเด่นในหน้าโครงการ:
- อัลกอริทึมแฮช: SHA2, SHA3, SHA1 และ MD5 ทุกรูปแบบ
- รหัสการตรวจสอบความถูกต้อง: HMAC บน SHA1, SHA2-256, SHA2-384 และ SHA2-512 สำหรับการตรวจสอบแหล่งข้อมูล
- อัลกอริทึมการสร้างคีย์ HKDF (ฟังก์ชันการสกัดและขยายคีย์การขยายตาม HMAC)
- การเข้ารหัสสตรีม ChaCha20 (มีเวอร์ชัน C ที่ไม่ได้ปรับให้เหมาะสม)
- อัลกอริธึมการตรวจสอบข้อความ Poly1305 (MAC) (เวอร์ชัน C และแอสเซมเบลอร์)
- โปรโตคอล Diffie-Hellman บนเส้นโค้งรูปไข่ Curve25519 (เวอร์ชัน C และแอสเซมเบลอร์พร้อมการปรับให้เหมาะสมตามคำแนะนำ BMI2 และ ADX)
- บล็อกโหมดการเข้ารหัส AEAD (การเข้ารหัสที่พิสูจน์ตัวตน) ChachaPoly (เวอร์ชัน C ไม่ได้รับการปรับให้เหมาะสม)
- โหมดการเข้ารหัสบล็อก AEAD AES-GCM (เวอร์ชันแอสเซมเบลอร์พร้อมการเพิ่มประสิทธิภาพ AES-NI)
ในครั้งแรก เวอร์ชันอัลฟ่าการยืนยันรหัสเสร็จสมบูรณ์แล้ว ส่วนใหญ่ แต่ยังมีบางพื้นที่ที่ถูกเปิดเผย
นอกจากนี้ API ยังไม่เสถียรซึ่งจะขยายออกไป ในเวอร์ชันอัลฟาต่อไปนี้ (มีการวางแผนที่จะรวมโครงสร้างสำหรับ API ทั้งหมด
ในบรรดาข้อบกพร่องการสนับสนุนสำหรับสถาปัตยกรรม x86_64 ยังได้รับการเน้นย้ำ (ในขั้นแรกเป้าหมายหลักคือความน่าเชื่อถือในขณะที่การเพิ่มประสิทธิภาพและแพลตฟอร์มจะถูกนำมาใช้ในอันดับที่สอง)
Fuente: https://jonathan.protzenko.fr