虚拟机是平台无关字节码程序的解释执行环境，是当今网络软件和计算设备中广泛使用的重要技术。 针对字节码程序和虚拟机平台的程序验证研究，可以提高相关软件的可信程度，具有重要的实用价值和理论价值。虽然近年提出了一系列用于字节码程序的逻辑系统，但是缺乏针对虚拟机实现的可信验证工作。因此即便是已验证字节码程序，一旦虚拟机出错依然无法正确运行。本文给出一种虚拟机构造和验证方案：1)给出字节码程序运行环境BCM(ByteCode Nachine)的形式化定义：2)采用机器语言构造虚拟机CertVM (Certified VirtualMachine)，并基于FPCC (Foundational Proof-CarryingCode)方法证明该虚拟机符合相应程序规范：3)证明虚拟机的实现程序和BCM之间具有模拟关系，并利用辅助工具Coq给出证明，所有证明均可机器自动检查。CertVM能够确保“只要硬件环境不出问题，已验证的字节码程序能够在给定虚拟机环境中正常运行”。本文给出的可信虚拟机构造方案，为广泛使用的一类复杂网络应用程序的深入分析、准确验证和可信运行提供理论帮助，同时为可信软件构造问题的解决提供一种良好思路和有益尝试。