หน้าแรก>การเขียนโปรแกรมที่เกี่ยวข้อง>ซอร์สโค้ดอื่น ๆ
ดาวน์โหลด

VeriSMo: โมดูลความปลอดภัยที่ได้รับการตรวจสอบอย่างเป็นทางการสำหรับ VM ที่เป็นความลับของ AMD

repo นี้รวมโค้ดสำหรับโครงการ VeriSMo

ไฟล์ ?

  • tools/ : รวมเครื่องมือตรวจสอบและคอมไพเลอร์และสคริปต์

  • deps/ : รวมแพ็คเกจ hacl

  • แหล่งที่มา/ : รหัส verismo

  • แหล่งที่มา/verismo : รหัสที่ตรวจสอบแล้วสำหรับ verismo

  • source/verismo_main : main executable bin ซึ่งกำหนดเฉพาะตัวจัดการ Rust panic ที่ไม่ได้รับการยืนยันเท่านั้น

  • แหล่งที่มา/verismo/src/arch : model

  • source/verismo/src/entry.s : รหัสแอสเซมบลีขนาดเล็กและไม่ได้รับการยืนยัน

  • source/target.json : การกำหนดค่าเป้าหมาย

0. ข้อกำหนดเบื้องต้น

ขั้นแรกให้ติดตั้งห่วงโซ่เครื่องมือที่เป็นสนิม 

tools/install.sh

1. ติดตั้งเครื่องมือ ?

จากนั้น สร้างเครื่องมือ verus, verus-rustc (แทนที่rustc) และ igvm และการขึ้นต่อกัน 

tools/activate.sh

2. ตรวจสอบและสร้าง

ตอนนี้ให้ดำเนินการตรวจสอบความถูกต้องและสร้างไบนารี่

- ขั้นตอนนี้ใช้เวลาหลายนาที

ก. ตรวจสอบโครงการทั้งหมด:

วิ่ง 

make verify

หรือ 

cd source/verismo_main; cargo verify --release;

ข. ในการตรวจสอบโมดูลเดียวซึ่งมีประโยชน์สำหรับการพัฒนา: 

cd source/verismo; verismo_VERUS_ARGS="--verify-module security::monitor" cargo verify --release;

ค. ทำความเข้าใจผลลัพธ์:

ผลลัพธ์ที่ได้รับการยืนยันอย่างครบถ้วนควรมี "ยืนยันแล้ว": 2138, "ข้อผิดพลาด": 0,

ง. สร้างโดยไม่มีการตรวจสอบ

หากไม่มีการเปลี่ยนแปลงใน source/verismo เราขอแนะนำให้สร้างโดยไม่มีการตรวจสอบเพื่อเร่งกระบวนการสร้างให้เร็วขึ้น 

make debugbuild

หรือ 

cd source/verismo_main; cargo build --feature noverify --release;

3. สร้างอิมเมจ VM (ข้ามหากคุณเรียกใช้ make หรือ make verify )

  1. ดาวน์โหลด linux submodule: git submodule update --init richos/snplinux

  2. สร้างระบบปฏิบัติการเกสต์และไดรเวอร์: make fs -f Makefile.default

  3. รัน sh source/target/target/release/verismo/igvm.sh เพื่อสร้าง verismo ในรูปแบบ IGVM สำหรับ Hyper-V: source/target/target/release/verismo/verismo-rust.bin

  4. เรียกใช้ make fs เพื่อสร้างไฟล์ vhdx เป็นระบบไฟล์สำหรับ VM: richos/test-fs/verismo.vhdx

4. ปรับใช้และรัน

ความต้องการ

  • ฮาร์ดแวร์: เครื่อง AMD SEV-SNP

  • ระบบปฏิบัติการ: Windows ที่มี Hypervisor เปิดตัวหลังปี 20230909 รุ่นก่อนหน้าอาจไม่รองรับการขัดจังหวะแบบจำกัดใน VMPL ทั้งสองรายการ ดังนั้นจึงจะไม่ทำงาน

  • ทางเลือก: เครื่องดีบักที่มีระบบปฏิบัติการ windows

ขั้นตอน

ย้ายไฟล์ต่อไปนี้ไปยังเครื่อง AMD SEV-SNP ของคุณ

  • source/target/target/release/verismo/verismo-rust.bin

  • richos/test-fs/verismo.vhdx

  • tools/vm/*

1. สร้าง SNP VM จาก PowerShell โดยได้รับอนุญาตจากผู้ดูแลระบบ 

build-vm.ps1 verismo verismo-rust.bin None verismo.vhdx

2. เริ่ม VM 

start-vm verismo

3. เชื่อมต่อกับแขก

ไม่รองรับการเข้าถึง GUI และคุณต้องใช้ ssh เพื่อเข้าสู่ระบบ guest OS

verismo.vhdx มีกระบวนการเริ่มต้นที่จะเปิดบริการ sshd โดยไม่ต้องใช้รหัสผ่าน

รอสักครู่ก่อนเชื่อมต่อ 

ssh [email protected]

4. พูดคุยกับโมดูล VeriSMo

เมื่อแขกบูตแล้ว จะมีการพูดคุยกับ VeriSMo เพื่อปลุก AP และอัปเดตสิทธิ์ของเพจในระหว่างการบูท

ภายในแขก เรายังจัดเตรียมไดรเวอร์ verismo และการทดสอบบางอย่างไว้เพื่อพูดคุยกับ VeriSMo โดยตรงหากคุณต้องการ

  • verismo.ko: คนขับ

  • decode_report: แสดงรายงานไบนารีในรูปแบบที่อ่านได้

  • test.sh: สคริปต์ทดสอบ 

cd verismo
insmod verismo.ko
sh test.sh

5. ตัวเลือกเสริม: คุณสามารถเข้าถึงบันทึกการบูตจาก VeriSMo ผ่านทางดีบักเกอร์ระยะไกล

โปรดดูการดีบักระยะไกลของ Windows เพื่อเปิดใช้งานการดีบักทั้งโฮสต์และไฮเปอร์ไวเซอร์ บันทึกการบูต VeriSMo ไม่สามารถเข้าถึงได้จากระบบปฏิบัติการเกสต์

กระบวนการสร้างทำงานอย่างไร?

แทนที่rustcด้วยverus-rustc

ใน source/.cargo/config.toml เราได้แทนที่rustc ด้วย verus-rustc verus-rustc จะเรียก verus เพื่อคอมไพล์ vstd (ไลบรารี verus), แพ็คเกจ verismo และ verismo-main และเรียก rustc เพื่อคอมไพล์แพ็คเกจอื่น ๆ ทั้งหมด (hacl, core ฯลฯ )

เพิ่ม build.rs เพื่อส่งตัวเลือกเพิ่มเติมไปยังเครื่องมือ verus

ดู source/verismo/build.rs

คุณสมบัติ

  • noverify: สร้างซอร์สโดยไม่มีการตรวจสอบ

  • ตรวจสอบโมดูล: หาก ${VERUS_MODULE} ไม่ว่างเปล่า ให้ตรวจสอบเฉพาะโมดูลที่ระบุเท่านั้น

ดีบักและรีลีส

ขึ้นอยู่กับ cfg(debug_assertations) โหมดดีบักจะพิมพ์ข้อความเพิ่มเติมเพื่อวัตถุประสงค์ในการแก้ไขจุดบกพร่องผ่าน Leak_debug โหมด Release จะลบข้อมูล Leak_debug หรือ Debug ทั้งหมด

มีส่วนร่วม

โครงการนี้ยินดีรับการสนับสนุนและข้อเสนอแนะ การบริจาคส่วนใหญ่กำหนดให้คุณต้องยอมรับข้อตกลงใบอนุญาตช่างภาพ (CLA) โดยประกาศว่าคุณมีสิทธิ์ที่จะให้สิทธิ์แก่เราในการใช้การบริจาคของคุณจริงๆ สำหรับรายละเอียด โปรดไปที่ https://cla.opensource.microsoft.com

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

โครงการนี้ได้นำหลักจรรยาบรรณของ Microsoft Open Source มาใช้ สำหรับข้อมูลเพิ่มเติม โปรดดูคำถามที่พบบ่อยเกี่ยวกับจรรยาบรรณหรือติดต่อ [email protected] หากมีคำถามหรือความคิดเห็นเพิ่มเติม

เครื่องหมายการค้า

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

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