이 저장소에는 VeriSMo 프로젝트용 코드가 포함되어 있습니다.
tools/ : 검증 도구, 컴파일러 도구 및 스크립트가 포함되어 있습니다.
deps/ : hacl 패키지를 포함합니다.
출처/ : 베리스모 코드
source/verismo : verismo에 대한 검증된 코드
source/verismo_main : 검증되지 않은 Rust 패닉 핸들러만 정의하는 주요 실행 파일입니다.
소스/verismo/src/arch : 모델
source/veismo/src/entry.s : 작고 검증되지 않은 어셈블리 코드입니다.
source/target.json : 대상 구성
먼저 Rust 툴체인을 설치합니다.
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
게스트 OS 및 드라이버 빌드: make fs -f Makefile.default
sh source/target/target/release/verismo/igvm.sh 실행하여 Hyper-V용 IGVM 형식의 verismo를 생성합니다: source/target/target/release/verismo/verismo-rust.bin
make fs 실행하여 VM용 파일 시스템으로 vhdx 파일을 생성합니다: richos/test-fs/verismo.vhdx
하드웨어: AMD SEV-SNP 머신.
OS: 20230909 이후에 출시된 하이퍼바이저가 있는 Windows. 이전 릴리스는 두 VMPL 모두에서 제한된 인터럽트를 지원하지 않을 수 있으므로 작동하지 않습니다.
선택 사항: Windows OS가 설치된 디버그 머신.
다음 파일을 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
GUI 액세스는 지원되지 않으며 게스트 OS에 로그인하려면 SSH를 사용해야 합니다.
verismo.vhdx에는 비밀번호 없이 sshd 서비스를 여는 init 프로세스가 포함되어 있습니다.
연결하기 전에 잠시 기다리십시오.
ssh [email protected]
게스트가 부팅되면 이미 VeriSMo와 통신하여 부팅 중에 AP를 깨우고 페이지 권한을 업데이트합니다.
게스트 내부에서는 원하는 경우 VeriSMo와 직접 통신할 수 있도록 verismo 드라이버와 몇 가지 테스트도 제공했습니다.
verismo.ko: 드라이버
decode_report: 바이너리 보고서를 읽을 수 있는 형식으로 표시합니다.
test.sh: 테스트 스크립트
cd verismo insmod verismo.ko sh test.sh
호스트 및 하이퍼바이저 디버깅을 모두 활성화하려면 Windows 원격 디버그를 참조하세요. VeriSMo 부팅 로그는 게스트 OS에서 액세스할 수 없습니다.
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를 통해 디버그 목적으로 추가 메시지를 인쇄합니다. 릴리스 모드에서는 모든 Leak_debug 또는 디버그 정보가 지워집니다.
이 프로젝트는 기여와 제안을 환영합니다. 대부분의 기여는 귀하가 귀하의 기여를 사용할 수 있는 권리를 갖고 있으며 실제로 그렇게 하고 있음을 선언하는 기여자 라이센스 계약(CLA)에 동의해야 합니다. 자세한 내용을 보려면 https://cla.opensource.microsoft.com을 방문하세요.
끌어오기 요청을 제출하면 CLA 봇이 자동으로 CLA 제공이 필요한지 여부를 결정하고 PR을 적절하게 장식합니다(예: 상태 확인, 댓글). 봇이 제공하는 지침을 따르기만 하면 됩니다. CLA를 사용하여 모든 저장소에서 이 작업을 한 번만 수행하면 됩니다.
이 프로젝트는 Microsoft 오픈 소스 행동 강령을 채택했습니다. 자세한 내용은 행동 강령 FAQ를 참조하거나 추가 질문이나 의견이 있는 경우 [email protected]으로 문의하세요.
이 프로젝트에는 프로젝트, 제품 또는 서비스에 대한 상표나 로고가 포함될 수 있습니다. Microsoft 상표 또는 로고의 승인된 사용에는 Microsoft의 상표 및 브랜드 지침이 적용되며 이를 따라야 합니다. 이 프로젝트의 수정된 버전에 Microsoft 상표 또는 로고를 사용하면 혼동을 일으키거나 Microsoft 후원을 암시해서는 안 됩니다. 제3자 상표 또는 로고의 사용에는 해당 제3자의 정책이 적용됩니다.
