【关注】望安科技受邀参加2023 CCF中国软件大会，W-AVC和W-Cert工具亮相会场！
来源:
|
作者:望安科技
|
发布时间: 289天前
|
651 次浏览
|
分享到:
12月2日，由中国计算机学会（CCF）主办，CCF系统软件专委会、形式化方法专委会、软件工程专委会、复旦大学承办的2023 CCF中国软件大会(ChinaSoft 2023)在上海国际会议中心正式开幕。
CCF中国软件大会是我国软件领域规模最大、影响力最广的学术会议。本届大会聚焦“智能化软件创新推动数字经济与社会发展”主题，包含学术、工业、教育以及竞赛四大类50余场活动，吸引来自十个国家和地区的高校、科研机构、企事业单位的2300余位专家学者参会交流学术，深度碰撞思想，以期超前谋划，踩准步点，推动我国软件技术与产业发展。
望安科技作为系统形式化验证与安全认证的推动者，受邀参加了本次大会，并由创始人-赵永望做了安全攸关软件形式化验证工具的专题报告，介绍了望安形式化验证工具W-AVC和W-Cert的独特优势。两个工具的亮相在会场引起了热烈的反响和广泛的关注。
望安C代码自动验证平台W-AVC是由望安科技研发的C语⾔代码程序的形式化验证云平台。平台基于形式化验证技术，通过数学证明排查代码中的缺陷和安全隐患；同时通过开发验证⼈员编写的规约基准代码，⾃动检查代码中的安全漏洞，从而在开发流程的早期增强系统的安全性，减少现代⼤型软件架构带来的⻛险。
1.形式化验证：望安W-AVC采用学界领先的形式化验证技术，无需专门设计测试用例，验证通过可百分百确保规约满足性，用数学证明保证无漏洞。
2.云端部署：项目云端验证，支持私有云部署，省去繁琐环境配置工作。随地登录验证，随时同步验证进度，支持私有云等相关定制化服务。
3.C语法规约：规约完全采用C语言语法，无需为消耗额外学习成本，开发测试人员无缝上手。工具提供内存、算术安全相关大量验证函数，使用方便、灵活。
4.规约分离：W-AVC实现了项目源代码与验证代码分离，验证代码不影响源码运行，提升开发/验证管理效率。项目代码区与验证代码区隔离，开发验证互不干扰。规约代码可封装复用，提高验证效率。
5.项目管理：W-AVC支持多项目上传与管理，验证报告显示覆盖率数据和错误追踪日志。平台支持文件创建、删除、修改等基本操作。验证代码区可创建桩函数、验证辅助函数文件，让形式化验证工程化。
6.多线程任务：平台支持证任务并行验证和中断操作，全方位升级验证工程效率。工具提供验证任务的批量验证、筛选、查看、取消等管理功能。
望安科技形式化验证工具W-Cert面向形式化建模与验证，可以有效支持从安全要求、安全策略、安全功能规范到安全设计的形式化建模与验证，并提供CC评估所需的形式化证据。W-Cert可基于CC标准推荐使用的lsabelle定理证明器，提供安全性质所需的一阶高阶逻辑描述方法、安全策略模型和功能规范所需的抽象状态机统一建模。
W-Cert工具具备设计模型所需的State Monad模型描述语言，以及支持CC证据所需的一致性、符合性和安全性的逻辑推理系统。可极大降低开发人员对形式化验证技术和CC形式化要求的掌握，使其重点关注产品本身的模型和验证。
1.可极大降低开发人员对形式化验证技术和CC形式化要求的掌握；
2.可完成覆盖需求、设计、源代码三个层次的形式化验证总体框架的开发；
3.可以进行快速的逻辑验证及推理。
智能化软件是数字经济的灵魂载体，软件正成为信息化社会不可或缺的基础设施，“软件定义一切”日益成为一种现实。此次受邀参会，是望安科技在软件行业的一次重要展示。未来，望安科技将继续深耕形式化验证领域，不断加大科技创新力度，紧随软件创新发展变革趋势，助力中国软件产业做大做强，服务于数字经济高质量发展。
