Modex是一个模型提取器。用于从实现级 C 代码中机械地提取验证模型。 Modex中存在安全漏洞,该漏洞源于Modex v2.11 被发现在 xtract.c 的 set_create_id() 中包含一个 NULL 指针取消引用。