牛津大学的研究人员发表了一篇题为“A Formal CHERI-C Semantics for Verification”的技术论文。
文摘:
“CHERI-C通过增加硬件功能扩展了C编程语言，确保了一定程度的内存安全性，同时保持了效率。还可以将功能用于更高级别的安全措施，例如软件划分，必须正确使用以实现所需的安全保证。由于扩展改变了C语言的语义，需要新的理论和工具来推理CHERI-C代码并验证正确性。在这项工作中，我们提出了一个正式的内存模型，为CHERI-C程序提供了一个内存语义。我们提出了一个具有丰富性质的广义理论，适合于验证和其他类型的潜在分析。我们的理论得到了Isabelle/HOL形式化的支持，它还生成了内存模型的OCaml可执行实例。然后将验证和提取的代码用于实例化参数化Gillian程序分析框架，利用该框架可以对CHERI-C程序进行具体执行。该工具可以运行CHERI- c测试套件，证明我们工具的正确性，并捕捉到CHERI硬件可能错过的一类安全违规行为。”
找到这里是技术文件．2022年11月出版。
作者:Seung Hoon Park, Rekha Pai, Tom Melham。arXiv: 2211.07511 v1。
留下回复