Этот репозиторий включает код проекта VeriSMo.
инструменты/: включает инструменты и сценарии верификатора и компилятора.
deps/: включает пакет hacl
источник/: код verismo
source/verismo: проверенный код для verismo
source/verismo_main: основной исполняемый файл, который определяет только непроверенный обработчик паники Rust.
источник/verismo/src/arch: модель
source/verismo/src/entry.s: небольшой и непроверенный ассемблерный код.
source/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 , чтобы сгенерировать веризмо в формате IGVM для Hyper-V: source/target/target/release/verismo/verismo-rust.bin
Запустите make fs , чтобы создать файл VHDX в качестве файловой системы для виртуальной машины: richos/test-fs/verismo.vhdx
Аппаратное обеспечение: машина AMD SEV-SNP.
ОС: Windows с гипервизором, выпущенным после 20230909. Более ранняя версия может не поддерживать ограниченные прерывания в обоих VMPL и, следовательно, не будет работать.
Дополнительно: машина отладки с ОС 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 включает процесс инициализации, который откроет службу sshd без пароля.
Подождите минуту перед подключением.
ssh [email protected]
После загрузки гость уже связался с VeriSMo, чтобы разбудить точку доступа и обновить разрешения страницы во время загрузки.
В гостевой системе мы также предоставили драйвер verismo и несколько тестов для прямой связи с VeriSMo, если хотите.
verismo.ko: водитель
decode_report: отображает двоичный отчет в читаемом формате.
test.sh: скрипт тестирования
cd verismo insmod verismo.ko sh test.sh
Обратитесь к удаленной отладке Windows, чтобы включить отладку как хоста, так и гипервизора. Журнал загрузки VeriSMo недоступен из гостевой ОС.
В исходном файле source/.cargo/config.toml мы заменили Rustc на Verus-rustc. verus-rustc вызовет verus для компиляции vstd (библиотеки verus), пакетов verismo и verismo-main , а также rustc для компиляции всех остальных пакетов (hacl, core и т. д.).
См. source/verismo/build.rs
noverify: собрать исходный код без проверки
verifymodule: если ${VERUS_MODULE} не пуст, проверяется только указанный модуль.
Зависит от cfg(debug_assertations). В режиме отладки дополнительные сообщения для целей отладки печатаются через Leak_debug; В режиме Release стирается вся информация Leak_debug или отладочная информация;
Этот проект приветствует вклад и предложения. Большинство вкладов требуют от вас согласия с Лицензионным соглашением для авторов (CLA), в котором говорится, что вы имеете право и действительно предоставляете нам права на использование вашего вклада. Подробную информацию можно найти на странице https://cla.opensource.microsoft.com.
Когда вы отправляете запрос на включение, бот CLA автоматически определяет, нужно ли вам предоставить CLA, и соответствующим образом оформляет PR (например, проверку статуса, комментарий). Просто следуйте инструкциям бота. Вам нужно будет сделать это только один раз во всех репозиториях, используя наш CLA.
В этом проекте принят Кодекс поведения Microsoft с открытым исходным кодом. Для получения дополнительной информации см. часто задаваемые вопросы о Кодексе поведения или свяжитесь с нами по адресу [email protected], если у вас возникнут дополнительные вопросы или комментарии.
Этот проект может содержать товарные знаки или логотипы проектов, продуктов или услуг. Разрешенное использование товарных знаков и логотипов Microsoft регулируется и должно соответствовать Руководству Microsoft по товарным знакам и брендам. Использование товарных знаков или логотипов Microsoft в измененных версиях этого проекта не должно вызывать путаницу или подразумевать спонсорство Microsoft. Любое использование товарных знаков или логотипов третьих лиц регулируется политикой этих третьих сторон.
