软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2010年
2期
305-317
,共13页
董渊%任恺%王生原%张素琴
董淵%任愷%王生原%張素琴
동연%임개%왕생원%장소금
已验证虚拟机%模块化验证%字节码%类Hoare逻辑
已驗證虛擬機%模塊化驗證%字節碼%類Hoare邏輯
이험증허의궤%모괴화험증%자절마%류Hoare라집
certified VM%modular certification%bytecode%Hoare-style logic
提出一种虚拟机构造和验证方案.给出字节码程序运行环境BVM(bytecode virtual machine)的形式化定义;采用X86机器语言构造虚拟机CertVM(certified virtual machine);并证明该虚拟机实现符合相应程序规范并和BVM之间具有模拟关系.利用辅助工具Coq给出证明,所有证明均可机器自动检查.CertVM确保在硬件环境满足其语义规范的情况下,已验证的字节码程序能够在给定虚拟机环境中正常运行.给出的方案不仅为虚拟机验证提供理论基础,而且为可信软件构造提供了一种有益的尝试.
提齣一種虛擬機構造和驗證方案.給齣字節碼程序運行環境BVM(bytecode virtual machine)的形式化定義;採用X86機器語言構造虛擬機CertVM(certified virtual machine);併證明該虛擬機實現符閤相應程序規範併和BVM之間具有模擬關繫.利用輔助工具Coq給齣證明,所有證明均可機器自動檢查.CertVM確保在硬件環境滿足其語義規範的情況下,已驗證的字節碼程序能夠在給定虛擬機環境中正常運行.給齣的方案不僅為虛擬機驗證提供理論基礎,而且為可信軟件構造提供瞭一種有益的嘗試.
제출일충허의궤구조화험증방안.급출자절마정서운행배경BVM(bytecode virtual machine)적형식화정의;채용X86궤기어언구조허의궤CertVM(certified virtual machine);병증명해허의궤실현부합상응정서규범병화BVM지간구유모의관계.이용보조공구Coq급출증명,소유증명균가궤기자동검사.CertVM학보재경건배경만족기어의규범적정황하,이험증적자절마정서능구재급정허의궤배경중정상운행.급출적방안불부위허의궤험증제공이론기출,이차위가신연건구조제공료일충유익적상시.
