多执行格点的快与慢
密码学与安全
2021-03-26 v1
摘要
自动、可靠且精确地保证非干涉安全策略的方法主要基于多执行。所有其他方法要么基于不可判定的定理证明，要么遭受误报之苦。与此同时，多执行机制通过在程序执行期间隔离安全级，并运行目标程序的多个副本（每个安全级一次，配以精心定制的输入以确保可靠性与精确性）来工作。当安全级在格点中分层组织时，由于组合安全级的可能方式增多，这可能导致目标程序的指数级执行次数。本文研究安全级的格点结构如何影响多执行的运行时开销。此外，我们展示了如何利用 Galois 连接通过从高空开销格点切换到低开销格点来在多执行中获得加速。另外，我们给出了一个实证评估，证实了我们的分析并展示了 Galois 连接加速多执行的潜力。
引用
@article{arxiv.2103.13667,
title = {Multi-Execution Lattices Fast and Slow},
author = {Maximilian Algehed and Cormac Flanagan},
journal= {arXiv preprint arXiv:2103.13667},
year = {2021}
}