现代网络浏览器(如Firefox或Chrome)有一个相当不错的功能，如果用户碰巧导航到恶意url，浏览器会自动警告用户：
虽然概念上很简单，但这个功能实际上需要比人们预期的更多的工程工作-特别是，以实际的方式跟踪已知的恶意URL集被证明是多么困难。
这是因为，一方面，试图存储所有已知恶意URL的数据库(记住，可能包含数百万个条目)对于大多数用户来说实际上是不可行的。
相反，将用户访问的每个URL发送到某个外部服务，在那里可能会被邪恶的第三方(即Google)记录和数据挖掘，这可能会让大多数用户感到不舒服。
事实证明，浏览器实际上是通过一种相当有趣的折衷方式来实现此功能的。
使用称为Bloomfilter的概率数据结构，浏览器在本地维护已知恶意URL集的近似表示。通过查询这个节省空间的本地集合，浏览器将只发送一小部分实际上很可能是恶意的URL。
使用Bloomfilter充当查询外部数据库的本地代理。
这种每天保护数百万用户隐私的代理技术依赖于Bloomfilter的两个关键属性：
这说明如果对Bloomfilter中的URL的查询返回否定，则可以保证所查询的项不存在于恶意URL集合中-即，Bloomfilter保证对所有已知的恶意URL返回肯定的结果。
此属性规定，对于不在恶意URL集中的任何URL，Bloomfilter查询返回正结果的可能性应该非常低-从而将不必要的侵犯用户隐私的次数降至最低。
这个机制工作得很好，布隆过滤器的保证似乎非常适合这个特殊的任务，但是它有一个小问题，那就是：
事实上，事实证明，布隆过滤器的行为实际上是长达30年的数学争论的主题，需要多次修正，甚至需要修正这些修正。
考虑到这段错误的历史，我们对Bloomfilter的理解真的有把握吗？
嗯，别害怕，我写这篇文章是想告诉你，我们最近刚刚使用Coq产生了第一个通过认证的Bloomfilter假阳性率证明，终于结束了这一错误传奇，让无数人每天都依赖的机制恢复了确定性(请原谅双关语1)。
在这篇文章的其余部分，我们将探讨这项研究的主要亮点，回答以下问题：
这项研究最近刚刚在CAV2020上发表，题目是“认证近似成员资格结构中的确定性和不确定性”，你可以在这里找到论文，以及这里的视频演示。
本研究项目中使用的代码和证明均为自由/开源软件，可在陶艺家资源库：https://github.com/certichain/ceramist上找到。
要将Bloomfilter用作近似集合，我们可以按如下方式执行标准集合操作：
要将一个值插入到布隆过滤器中，只需对每个哈希函数进行哈希运算，并将哈希输出作为位向量的索引，提高相应的位。
要查询Bloomfilter中的值，请再次对每个哈希函数进行哈希运算，然后检查是否引发了所有相应的位。
这些操作虽然相当简单，但实际上完全足以确保无假阴性属性(有关Coq语句，请参阅此处)：
当项目被插入Bloomfilter时，它将导致位向量中的某些位的子集被引发。由于没有可以取消设置这些位的操作，我们可以确定对插入的元素的任何后续查询都必须返回TRUE。换句话说，如果查询得到否定的结果，我们可以确定该项目以前从未插入过Bloomfilter。
这就是负面结果的情况；由于可能出现假阳性，对于正面结果来说，事情会变得稍微有趣一些。