论文标题
移动借用检查员
The Move Borrow Checker
论文作者
论文摘要
MOVE语言通过数字资产的编程提供了抽象，通过价值语义和参考语义的混合。确保具有参考的程序中的记忆安全，这些参考可以访问共享，可变的全局分类帐非常困难，但对于通过移动针对的用例来说至关重要。该语言通过新颖的记忆模型和一个模块化的静态静态参考安全性分析来应对这一挑战，该分析利用了记忆的关键特性。该分析可确保所有移动程序（包括针对不信任代码链接的程序）的不存在记忆安全性，作为加载时间字节bytecode验证通行证的一部分，类似于JVM [12]和CLR [15]。我们对静态分析进行了形式化，并证明它具有三种理想的特性：缺乏悬空的参考，不变参考的参考透明度以及缺乏记忆泄漏。
The Move language provides abstractions for programming with digital assets via a mix of value semantics and reference semantics. Ensuring memory safety in programs with references that access a shared, mutable global ledger is difficult, yet essential for the use-cases targeted by Move. The language meets this challenge with a novel memory model and a modular, intraprocedural static reference safety analysis that leverages key properties of the memory. The analysis ensures the absence of memory safety violations in all Move programs (including ones that link against untrusted code) by running as part of a load-time bytecode verification pass similar to the JVM [12] and CLR [15]. We formalize the static analysis and prove that it enjoys three desirable properties: absence of dangling references, referential transparency for immutable references, and absence of memory leaks.
