Ahead-of-time algebraic compilation for safety-critical Java
Ahead-of-time algebraic compilation for safety-critical Java
复制标题
DOI：
--
复制
发表时间：
2018-07
期刊：
影响因子：
--
通讯作者：
James Baxter
中科院分区：
文献类型：
--
作者：
James Baxter
近年来，Java 越来越被认为是安全关键型嵌入式系统的语言。然而，Java 的某些功能不适合此类系统。这导致了安全关键 Java (SCJ) 的创建，它促进了可认证的实时和嵌入式 Java 程序的开发。 SCJ 使用与标准 Java 不同的调度和内存管理模型，因此它需要专门的虚拟机 (SCJVM)。一种常见的方法是提前将 Java 字节码程序编译为本机语言（通常是 C），以便在资源匮乏的嵌入式系统上获得更高的性能。考虑到应用程序的安全性，必须确保虚拟机的正确性。然而，到目前为止，形式化验证还没有应用于任何SCJVM。本论文通过提出从 Java 字节码到 C 的编译验证，有助于对利用提前编译的 SCJVM 进行形式化验证。我们采用的方法是对 Sampaio 和 Hoare 开发的代数方法的改编。我们从执行程序字节码的 SCJVM 的正式规范开始，并通过应用经过验证的编译规则将其转换为目标 C 代码的表示形式。因此，我们的贡献是 SCJVM 的正式规范、一组带有证明的编译规则以及应用这些编译规则的策略。我们的编译策略可以用作提前编译 SCJVM 实现或现有实现验证的基础。此外，我们的 SCJVM 正式模型可以用作创建解释型 SCJVM 的规范。为了确保我们结果的适用性，我们的工作基于icecap，这是当前唯一可用的开源 SCJVM，并且符合 SCJ 标准。
In recent years Java has been increasingly considered as a language for safety-critical embedded systems. However, some features of Java are unsuitable for such systems. This has resulted in the creation of Safety-Critical Java (SCJ), which facilitates the development of certifiable real-time and embedded Java programs. SCJ uses different scheduling and memory management models to standard Java, so it requires a specialised virtual machine (SCJVM). A common approach is to compile Java bytecode program to a native language, usually C, ahead-of-time for greater performance on low-resource embedded systems. Given the safety-critical nature of the applications, it must be ensured that the virtual machine is correct. However, so far, formal verification has not been applied to any SCJVM. This thesis contributes to the formal verification of SCJVMs that utilise ahead-of-time compilation by presenting a verification of compilation from Java bytecode to C. The approach we adopt is an adaptation of the algebraic approach developed by Sampaio and Hoare. We start with a formal specification of an SCJVM executing the bytecodes of a program, and transform it, through the application of proven compilation rules, to a representation of the target C code. Thus, our contributions are a formal specification of an SCJVM, a set of compilation rules with proofs, and a strategy for applying those compilation rules. Our compilation strategy can be used as the basis for an implementation of an ahead-of-time compiling SCJVM, or verification of an existing implementation. Additionally, our formal model of an SCJVM may be used as a specification for creating an interpreting SCJVM. To ensure the applicability of our results, we base our work on icecap, the only currently available SCJVM that is open source and up-to-date with the SCJ standard.