Idris中用于静态信息流控制的从属型库
1月29日 · 1 分钟阅读
原作者：Simon Gregersen，SørenEller Thomsen和Aslan Askarov —Aarhus大学
（发布于F.Nielson和D.Sands（编辑）：POST 2019，LNCS 11426，第51–75页，2019.）
在应用程序中安全地集成第三方代码，同时保护信息的机密性是一个长期存在的问题。
像Haskell这样的纯函数式编程语言，使得通过Russo处理像MAC这样的库，实现轻量级的信息流控制成为可能。
本文介绍了DepSec，这是一种受MAC启发，在Idris中用于静态信息流控制的从属型库。我们将展示添加从属类型如何增强最新的静态信息流控制库的表现力，以及DepSec如何匹配一个特殊用途的从属信息流类型系统。
最后，我们展示了使用从属类型指定静态强制解密策略的新颖而强大的方法。
要获取此科学论文的完整版本，请单击此处。
快来发现Concordium并加入我们的社区！
开发人员中心：https：//development.concordium.com/tech
Gitter：https : //gitter.im/concordium_official/community
