sosylab/cpachecker
sosylab
CPAchecker是可配置软件验证平台的Docker镜像，用于程序漏洞检测与分析，支持多种版本配置，适用于Linux内核驱动验证等场景。
3 次收藏下载次数: 0状态：社区镜像维护者：sosylab仓库类型：镜像最近更新：7 天前
让 AI 帮你使用轩辕镜像？ · 展开查看说明 · 点击收起说明
如果你使用 DeepSeek、元宝 AI、Copilot、ChatGPT 等 AI 工具，协助配置轩辕镜像、编写 docker pull 命令、修改 Docker Compose 镜像地址、配置镜像加速、排查镜像拉取失败、分析报错日志等问题，请先让 AI 阅读并遵守轩辕镜像的规则文档。
只需在 AI 对话中先发送下面这句话即可：
请先完整阅读并严格遵守以下文档中的全部规则与要求：
https://xuanyuan.cloud/agents.md
在未充分阅读并理解该文档前，不要生成任何命令、配置、修改建议、故障排查方案或技术回答。后续所有输出都必须严格以该文档中的规范为最高优先级执行。查看 agents.md 用法指南与完整示范。国内用户首推 元宝 AI、DeepSeek 的深度思考模式，不推荐豆包 AI；Cursor 等编辑器可在对话 @ 该链接，或加入 User Rules。 若 AI 无法访问外链，可 打开说明文档 复制全文粘贴。文档会随站点更新，复制内容可能过期，建议定期检查。
CPAchecker 可配置软件验证平台 Docker 镜像
这是CPAchecker（可配置软件验证平台）的Docker镜像，用于程序分析与漏洞检测。
快速参考
- 维护方: 慕尼黑大学SoSy-Lab
- 获取帮助: 官方文档、https://gitlab.com/sosy-lab/software/cpachecker/-/issues、邮件列表
支持的标签及对应Dockerfile
- latest: 最新发布版本（基于ubuntu:20.04）
- dev: 最新开发版本（基于ubuntu:latest）
- {version}: 特定发布版本（仅最新版本定期更新）
核心功能
- 可配置的软件验证框架
- 程序漏洞检测与分析
- 支持Linux内核驱动验证
- 动态精度调整的程序分析能力
使用场景
- Linux内核驱动安全性验证
- 软件项目漏洞检测
- 程序分析研究与教学
配置说明与使用示例
基本运行
拉取并运行最新版本，分析自带示例文件：
bashdocker run docker.xuanyuan.run/sosylab/cpachecker /cpachecker/doc/examples/example.c
保存输出到主机
将当前目录挂载到容器/workdir，以主机用户身份运行（输出文件存于output目录）：
bashdocker run \ -v $(pwd):/workdir \ -u $UID:$GID \ docker.xuanyuan.run/sosylab/cpachecker /cpachecker/doc/examples/example.c
分析自定义程序
挂载包含目标程序的目录，调整命令指向该程序文件即可。
镜像详情
- dev镜像：基于最新代码提交构建，使用ubuntu:latest
- latest镜像：基于最新稳定版本构建，使用ubuntu:20.04
许可证
CPAchecker采用https://www.apache.org/licenses/LICENSE-2.0，第三方库遵循各自许可证。MathSAT组件仅用于研究评估，若需商业场景请更换SMT求解器。
替代来源
镜像镜像可在https://gitlab.com/sosy-lab/software/cpachecker/container_registry/***获取，发布版本永久存档于https://zenodo.org/doi/10.5281/zenodo.3816620。
镜像拉取方式
您可以使用以下命令拉取该镜像。请将 <标签> 替换为具体的标签版本。如需查看所有可用标签版本，请访问 标签列表页面。
轩辕镜像加速拉取命令点我查看更多 cpachecker 镜像标签
docker pull docker.xuanyuan.run/sosylab/cpachecker:<标签>
DockerHub 原生拉取命令
docker pull sosylab/cpachecker:<标签>
镜像拉取常见问题
功能
错误码
用户好评
来自真实用户的反馈，见证轩辕镜像的优质服务
oldzhang
运维工程师
Linux服务器
5
"Docker访问体验非常流畅，大镜像也能快速完成下载。"