يتضمن هذا الريبو رمز مشروع VeriSMo.
Tools/ : تتضمن أدوات ونصوص برمجية للتحقق والمترجم.
deps/ : يتضمن حزمة hacl
المصدر/: كود فيريزمو
المصدر/verismo: رمز تم التحقق منه لـ verismo
source/verismo_main : الحاوية الرئيسية القابلة للتنفيذ، والتي تحدد فقط معالج ذعر Rust الذي لم يتم التحقق منه.
المصدر/verismo/src/arch : model
source/verismo/src/entry.s : رمز تجميع صغير لم يتم التحقق منه.
المصدر/target.json: تكوين الهدف
أولاً، قم بتثبيت سلسلة أدوات الصدأ؛
tools/install.sh
بعد ذلك، قم ببناء أدوات وتبعيات verus وverus-Rustc (لتحل محل Rustc) وIGVM.
tools/activate.sh
الآن، قم بإجراء عمليات التحقق من الصحة وقم ببناء الملف الثنائي.
؟ تستغرق هذه الخطوة عدة دقائق.
يجري
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;
make أو make verify ) تنزيل وحدة Linux الفرعية: git submodule update --init richos/snplinux
قم ببناء نظام التشغيل وبرامج التشغيل الضيف: make fs -f Makefile.default
قم بتشغيل sh source/target/target/release/verismo/igvm.sh لإنشاء verismo بتنسيق IGVM لـ Hyper-V: source/target/target/release/verismo/verismo-rust.bin
قم بتشغيل make fs لإنشاء ملف vhdx كنظام ملفات لجهاز VM: richos/test-fs/verismo.vhdx
الأجهزة: جهاز AMD SEV-SNP.
نظام التشغيل: تم إصدار Windows المزود ببرنامج Hypervisor بعد 20230909. قد لا يدعم الإصدار السابق المقاطعات المقيدة في كلا VMPLs وبالتالي لن يعمل.
اختياري: جهاز تصحيح يعمل بنظام التشغيل Windows.
انقل الملفات التالية إلى جهاز AMD SEV-SNP الخاص بك.
source/target/target/release/verismo/verismo-rust.bin
richos/test-fs/verismo.vhdx
tools/vm/*
build-vm.ps1 verismo verismo-rust.bin None verismo.vhdx
start-vm verismo
الوصول إلى واجهة المستخدم الرسومية غير مدعوم وتحتاج إلى استخدام ssh لتسجيل الدخول إلى نظام التشغيل الضيف.
يتضمن verismo.vhdx عملية init التي ستفتح خدمة sshd بدون كلمة مرور.
انتظر لمدة دقيقة قبل الاتصال.
ssh [email protected]
بمجرد تشغيل الضيف، فقد تحدث بالفعل مع VeriSMo لتنبيه نقطة الوصول وتحديث أذونات الصفحة أثناء التشغيل.
داخل الضيف، قمنا أيضًا بتوفير سائق veriSmo وبعض الاختبارات، للتحدث إلى VeriSMo مباشرة إذا كنت تريد ذلك.
verismo.ko: سائق
decode_report: عرض التقرير الثنائي بتنسيق قابل للقراءة.
test.sh: برنامج نصي للاختبار
cd verismo insmod verismo.ko sh test.sh
ارجع إلى تصحيح أخطاء Windows عن بعد لتمكين تصحيح أخطاء كل من المضيف وبرنامج Hypervisor. لا يمكن الوصول إلى سجل تمهيد VeriSMo من نظام التشغيل الضيف.
في source/.cargo/config.toml، استبدلنا ملف Rustc بـ verus-rustc. سوف يستدعي verus-rustc verus لتجميع vstd (مكتبة verus)، وحزمة verismo و verismo-main ، ويستدعي rustc لتجميع كل الحزم الأخرى (hacl، core، وما إلى ذلك).
انظر source/verismo/build.rs
noverify: بناء المصدر دون التحقق
Veremodule: إذا لم يكن ${VERUS_MODULE} فارغًا، فتحقق فقط من الوحدة المحددة.
يعتمد على cfg(debug_assertations) يقوم وضع التصحيح بطباعة رسائل إضافية لغرض التصحيح عبرتسرب_debug; يقوم وضع الإصدار بمسح كافة معلوماتتسرب البيانات أو معلومات تصحيح الأخطاء؛
يرحب هذا المشروع بالمساهمات والاقتراحات. تتطلب معظم المساهمات منك الموافقة على اتفاقية ترخيص المساهم (CLA) التي تعلن أن لديك الحق في منحنا حقوق استخدام مساهمتك، بل وتفعل ذلك بالفعل. للحصول على التفاصيل، تفضل بزيارة https://cla.opensource.microsoft.com.
عند إرسال طلب سحب، سيحدد روبوت CLA تلقائيًا ما إذا كنت بحاجة إلى تقديم CLA وتزيين العلاقات العامة بشكل مناسب (على سبيل المثال، التحقق من الحالة، التعليق). ما عليك سوى اتباع التعليمات التي يقدمها لك الروبوت. سوف تحتاج إلى القيام بذلك مرة واحدة فقط في جميع عمليات إعادة الشراء باستخدام CLA الخاص بنا.
اعتمد هذا المشروع قواعد السلوك الخاصة بشركة Microsoft مفتوحة المصدر. لمزيد من المعلومات، راجع الأسئلة الشائعة حول قواعد السلوك أو اتصل بـ [email protected] لطرح أي أسئلة أو تعليقات إضافية.
قد يحتوي هذا المشروع على علامات تجارية أو شعارات للمشاريع أو المنتجات أو الخدمات. يخضع الاستخدام المصرح به للعلامات التجارية أو الشعارات الخاصة بشركة Microsoft ويجب أن يتبع إرشادات العلامة التجارية والعلامات التجارية الخاصة بشركة Microsoft. يجب ألا يتسبب استخدام العلامات التجارية أو الشعارات الخاصة بشركة Microsoft في الإصدارات المعدلة من هذا المشروع في حدوث ارتباك أو الإشارة ضمنًا إلى رعاية Microsoft. ويخضع أي استخدام لعلامات تجارية أو شعارات تابعة لجهات خارجية لسياسات تلك الجهات الخارجية.
