“沙盒”一词很宽泛、通用，并且经常被误用和误解。

让我们考虑一种沙盒，一种在管理程序控制下运行的虚拟机。来宾系统名义上是隔离的，无法“看到”主机系统。然而，这与虚拟机管理程序的实现有关，它是软件和硬件的组合，两者都容易受到错误的影响（硬件总是涉及整个事情，最终运行在 CPU 上；我不是在说关于使用或不使用 AMD-V/Intel-VT 操作码）。已经发生了从管理程序中逃脱的事件。“证明”管理程序是正确的意味着证明它没有错误。在过去的半个世纪里，证明软件没有错误一直是一个相当难以实现的目标……对于硬件来说，更是如此。

此外，沙盒并不等同于安全。要使沙箱有用，它必须有几个敞开的门：您在沙箱中运行一些软件，但您会希望看到结果，无论是显示的内容、保存在某处的文件，还是一些网络活动。当人们在沙盒中使用 Web 浏览器时，他们希望浏览器能够实际浏览Web，因此必须允许来自沙盒的外部网络连接；并且沙盒浏览器也必须有显示东西的可能性，所以它可以访问图形硬件（可能是受控访问，但如果你想要 3D 加速，严格控制变得困难）。您想要一个沙箱，因为您怀疑浏览器可能被攻击者颠覆和劫持。但是，在那一点上，你已经输了（不是整场战争，而是重要的战斗）：被颠覆的浏览器，无论是否沙盒，都可以联网，可以用作攻击其他站点或发送垃圾邮件的中继，看似起源于从你的地址。

用更简洁的话来说，截肢并不是最终可取的药物类型。

让我们看看另一种沙箱，Java 虚拟机及其对小程序的支持。它有两个主要方面：

• “代码”不是本地 CPU 的原始二进制代码，而是“字节码”：概念抽象机器的操作码，它存在于不允许通用指针算术的非硬件世界中。引用具有不可避免的类型，并且数组访问是经过边界检查的。

• 小程序代码的外部访问设施受到限制：网络连接只能与始发服务器建立；无法读取或写入本地文件；等等。

当必须运行字节码时，首先对其进行分析：JVM 实现进行控制流分析，正式证明（是的，在“可证明的安全性”意义上）代码符合字节码的类型规则（即，它从不调用不具有该方法的对象的方法）。这允许转换为高效的本机代码，而无需专门的虚拟化硬件。此外，它可以防止多种类型的破坏（可靠地检测到缓冲区溢出，由于GC没有悬空指针或双释放基于内存管理...）。这种保护对于“安全”来说是不够的，因为您仍然需要由系统类强制执行的访问控制（例如，阻止与原始服务器的外部连接）。字节码分析是为了确保只使用系统类并正确使用；其余的取决于系统类。

当然，在 Java 的历史上，字节码分析器和系统类的实现都被发现存在缺陷。它们不是内在的：它们试图实现的目标在数学上并非不可能。但是，让我们面对现实：错误发生了。JVM 是一个相当复杂的软件，远没有被证明是没有错误的。此外，JVM 在操作系统和一些有形硬件上运行，它们都不是没有错误的。

这说明了我的观点：

• 沙盒仅在其实现没有错误的情况下才提供“可证明的安全性” 。这有点空想。
• 沙盒实际上提供的是一组规则的执行，这些规则可能或更经常地可能不体现您真正所说的“安全性”。像往常一样，正确安全的第一步是明确定义您想要什么。

假设您已经证明您的沙箱对所有攻击都是免疫的。如果这个证明是在大约 10 年前提出的，那么它就不会考虑悬空指针和填充预言机攻击，因为这些利用方法在当时是未知的。因此，您无法证明此沙盒是完全安全的，因为这将是矛盾的 -><-

您的问题似乎表明对安全性的误解。经验证的安全性是矛盾的。没有什么是完全安全的，或者正如旧的 IT 安全笑话所说，唯一可证明安全的存储是写入 dev/null（即销毁）。安全只是资源和成本的博弈。它试图平衡合法用户获取信息的需求，同时防止攻击者这样做，但只要有任何允许的访问权限，只要有足够的资源和时间，就总是有可能或至少是可行的，破坏系统并获得访问权限。

自毁系统试图通过限制可以完成的访问量来避免这个问题，但是只要有足够的资源和努力，创造性的方法就可以绕过其中的大部分（有时甚至可以降低到实际溶解芯片层的水平，一层一层）。

这个问题确实需要更多澄清才能回答。您的意思是，能否证明针对特定类型的攻击的保护？如果是这样，您担心什么样的攻击？

这取决于您谈论哪种可证明的安全性（无论是不可能的还是胡说八道）。但是在安全算法中，可证明的安全性意味着为了破解你的算法，需要有人破解底层加密货币。因此，如果我们认为我们的加密算法是安全的，并且你写了一个证明，证明只有通过破解密码你才能破解你的算法，那么它没有任何意义，它只是可以研究和发布的东西而已. 我同意 Rook 攻击模式正在演变，这证明现在在十年左右的时间内不会安全。