Agda形式化：非干涉翻译与安全信息流类型系统

本文主要探讨了在理论计算机科学领域中，Agda形式化方法在信息流类型系统中的应用，特别是关注如何实现静态实施安全保护策略，如无干扰原则。信息流分析是一种关键的技术，用于保护数据隐私，防止通过公共数据推测出私人信息。无干扰策略强调的是，当两个计算结果仅在私密输入上有所差异时，程序不应在执行过程中泄露任何非法信息流。 作者塞西莉亚·曼齐诺和阿尔贝托·帕尔多在阿根廷罗萨里奥国立大学和乌拉圭蒙得维的亚大学计算机学院合作，利用了Agda这种依赖类型的编程语言进行形式化研究。Agda的类型系统以其强大的表达能力被用来编码安全类型系统，使得程序在类型级别上就能确保安全性。他们的工作重点在于Hunt和Sands翻译的无干扰保存，这是一种将高级别的程序类型转换到低敏感类型系统的过程，同时保持等价性和安全性。 这个形式化研究采用了一种完全内在的方法，通过装饰类型的抽象语法来直接反映安全类型信息，确保只有符合安全要求的程序才能获得良好类型。这种方法的优势在于，它不仅表达了程序之间的转换关系，而且作为安全保护的归纳证明，可以直接体现在转换关系的类型层面上。 论文的关键词包括无干扰、信息流类型系统、依赖类型编程、Agda以及类型安全。值得注意的是，该研究是基于Creative Commons Attribution-NonCommercial-NoDerivatives (CC BY-NC-ND) 许可证的开放获取文章，可以在Elsevier的网站<https://doi.org/10.1016/j.entcs.2020.08.005>上获取，发表在《电子笔记》(Electronic Notes in Theoretical Computer Science) 351期，75-94页。这一工作展示了如何将理论研究成果转化为实践，并在实际的编程语言工具中实现安全性和隐私保护。