django-coex:Django 应用程序的 Concolic 执行

该项目旨在为 Django Web 应用程序构建一个 concolic 执行检查器。 Concolic 执行可用于验证系统的某些不变量是否成立（例如，除非交易被记录，否则钱永远不会离开银行），而不会产生全面的符号检查成本。 最初，目标是让检查器适用于此处托管的 Zoobar 演示应用程序的 Django 版本： : 。 虽然我们想尽量避免对 Django 进行更改来实现这一点，但我们在维护了一个单独的分支，目前基于 1.7 稳定版，其中可能包括获得 concolic 所需的修改执行以正常工作。 该代码主要基于（MIT 许可的）concolic 执行框架，该框架为 MIT 2014 年秋季 6.858 类计算机安全中的构建。 要为 Zoobar 启动并运行 django-coex，请执行以下操作： $ git clone https://github.com/jonhoo/dj