Modex是一个模型提取器。用于从实现级 C 代码中机械地提取验证模型。 Modex中存在安全漏洞,该漏洞源于通过组件 tcache 发现 Modex v2.11 包含一个 Use-After-Free 漏洞。