Security Engineering in IIIf, Part II -- Shadowing the IIIf
本文通过引入 Morgan 的“影子”（Shadow）概念来形式化信息流安全，从而扩展了 Isabelle Insider and Infrastructure 框架（IIIf）的安全工程，进而解决了细化悖论，并确立了通过飞行雷达系统示例所阐明的安全细化条件。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
大局观： “飞行雷达”问题
想象一下，你正在手机上查看一个公开的飞行雷达应用。你看到飞机在地图上移动。通常情况下，这是无害的。但如果一架飞机突然在某个特定区域周围进行奇怪的、之字形的绕行呢？
在现实世界中，飞机不会为了好玩而随意改变航线。如果一架飞机突然绕开某个秘密军事基地或 VIP 的所在地，这种“绕行”就是一个线索。即使应用没有向你展示那个秘密基地，飞机的运动模式也会准确地告诉你危险区域在哪里。
这就是这篇论文要解决的问题：我们如何阻止秘密信息通过系统行为的副作用“泄露”出来？
角色与设定
- 系统 (IIIf)： 可以把它想象成一个巨大的、极其严格的数字城市规则手册。它追踪谁在哪里、他们遵循什么规则以及事物是如何移动的。作者使用了一个名为“Isabelle”的强大计算机工具来编写这个规则手册，使其足够严密，以至于计算机可以证明其正确性。
- 攻击者 (Eve)： Eve 是一个爱管闲事的观察者，她可以看到系统向公众展示的一切内容（比如地图上的飞机位置），但不应该知道那些秘密（比如秘密基地的位置）。
- 秘密 (关键位置/Critical Location)： 这是系统试图保护的“禁区”。
问题：“细化悖论” (The Refinement Paradox)
作者解释了一个棘手的现象，称为细化悖论。
想象一下，你设计了一个安全的系统（“抽象”版本）。你向计算机证明了 Eve 无法猜到秘密。太棒了！
然后，你决定让系统变得更好或更详细（“细化”版本）。也许你添加了一个新功能，比如显示飞机的速度。
悖论在于： 即使你的新功能看起来是无害的，它也可能意外地创造出一个新的“泄露点”。
- 类比： 想象你把一张秘密纸条藏在一个保险箱里。你证明了保险箱是安全的。然后，你决定在保险箱上添加一个微小的装饰性把手。你并没有改变锁，但现在，如果你摇晃保险箱，把手发出的响声会根据纸条在内部的位置而不同。突然间，这个把手泄露了秘密。
在论文的例子中，如果系统是基于飞机的真实（隐藏的）路径而不是其公开路径来计算速度，那么每当飞机避开秘密区域时，速度数值就会变得很奇怪。Eve 看到了这个奇怪的速度，并立刻知道了秘密区域的位置。系统变得“更详细”了，但也变得更不安全了。
解决方案：“影子” (The Shadow)
为了修复这个问题，作者引入了一个受数学家 Morgan 启发的概念，称为影子 (Shadow)。
什么是影子？
可以将影子想象成一个关于秘密信息的**“可能性之袋”**。
- 在开始时，影子是一个巨大的袋子，里面装满了关于秘密可能位置的所有可能性。攻击者完全处于困惑状态；他们根本不知道秘密在哪里。
- 随着系统的运行，影子应该保持很大。如果影子缩小了，这意味着攻击者了解到了新的信息。
目标： 一个安全的系统是指其影子永不缩小。如果影子保持不变的大小，攻击者的无知状态就能得到保留。他们掌握的信息并不会比最初时更多。
他们如何修复飞行雷达
作者将这个“影子”概念应用到了他们的飞行雷达系统中：
- 泄露点： 在原始的不安全版本中，飞机的运动揭示了秘密位置。由于攻击者可以根据飞机的路径排除某些位置，导致影子缩小了。
- 修复方法： 他们添加了一个“隐藏”机制。当飞机需要避开秘密区域时，系统会在一个秘密盒子（
critpos组件）中记录真实路径，但在公开地图上显示飞机仿佛是直行穿过了秘密区域。 - 结果： 因为公开地图看起来很正常，攻击者的“可能性之袋”（影子）永远不会变小。攻击者仍然认为秘密区域可能在任何地方。
“神奇”的证明
论文主要做了两件事：
- 等价性： 他们证明了“影子永不缩小”与“非干预性 (Non-Interference)”（一个高级技术术语，意为“秘密不会影响公众所见的内容”）是完全等价的。这就像是在证明“袋子始终是满的”等同于“没有人偷走苹果”。
- 升级的安全规则： 他们创建了一个规则（定理 2）来检查未来的升级（细化）是否能保持安全。
- 规则： 如果你添加一个新功能，你必须检查该功能是否依赖于该秘密。如果新功能依赖于该秘密，影子就会缩小，那么这次升级是不安全的。
- 关键点： 如果这个新功能完全独立于该秘密，影子就会保持不变，那么升级就是安全的。
总结
这篇论文解决了一个问题，即让系统变得更详细的过程可能会意外泄露秘密。他们使用“影子”（可能性之袋）来追踪攻击者所知道的信息。如果影子保持充盈，系统就是安全的。他们证明了，如果在添加新功能时遵循他们特定的规则，你就可以在不意外泄露秘密的情况下升级系统。
简而言之： 他们构建了一个数学上的“保安”，每当你为系统添加新功能时，这个保安都会进行检查，确保新功能不会在无意中向公众“低声耳语”那些秘密。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。