Formal proof of an integrated hardware garbage collector

集成硬件垃圾收集器的正式证明

• 批准号: 1942419
• 金额: --
• 依托单位: University of Bristol
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2017
• 资助国家: 英国
• 起止时间: 2017 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-1942419
• 关键词: Formal; proof; integrated; hardware; garbage

The Integrated Hardware Garbage Collector is an innovative new design for hardware garbage collection which promises to significantly improve system security and reliability by replacing traditional MMUs. It achieves this by replacing the traditional flat address space memory model with a new object-based sparsely-connected memory model. This entirely prevents buffer overflow issues and similar classes of errors and vulnerabilities. In addition, it can offer real-time performance for high level languages such as Java, C# and Haskell. However, without strong guarantees of correctness the design cannot be trusted in general purpose applications. To provide these guarantees, this thesis formally proves the correctness of the IHGC design for both an abstract model and a Verilog implementation.

集成硬件垃圾收集器是一种创新的硬件垃圾收集新设计，有望通过取代传统的mmu来显著提高系统的安全性和可靠性。它通过用一种新的基于对象的稀疏连接内存模型取代传统的平面地址空间内存模型来实现这一点。这完全防止了缓冲区溢出问题和类似类型的错误和漏洞。此外，它还可以为Java、c#和Haskell等高级语言提供实时性能。然而，在一般用途的应用程序中，如果没有强有力的正确性保证，设计就不能被信任。为了提供这些保证，本文从抽象模型和Verilog实现两方面正式证明了IHGC设计的正确性。