案例研究

该企业提供了智能驾驶领域的定制解决方案。借助其专有的AI处理器和计算平台，他们可以提供外部环境感知，车载多模式交互以及高精度地图建模。

由于该企业现有扫描工具仅覆盖 MISRA规则，一些重要的内存有关的致命缺陷（如数组越界（AOB ）和空指针解引用（NPD）等），在编码期间无法被检测到。据统计，约30%的开发时间被浪费在查找错误和分析原因上，这样的缺陷也极大影响了开发效率。

如上所述，现有Linux系统普遍有的内存问题，它的可靠性和安全性慢慢难以满足如无人驾驶等更高的业务要求，形式化验证过的seL4微内核能提供更好的效果。

通过将爱科识集成到软件开发生命周期（SDLC）中，并采用鉴释的安全编码，该企业可以精准、快速识别出关键问题，包括AOB和NPD。通过使用自定义规则，该企业避免了常规测试中不容易发现的业务逻辑问题。

鉴释提供专业的MISRA合规的技术和流程支持，如从规则解释分类/过滤/辩解证明报告等，合作打造起不但形式化安全认证过还ASIL-D合规以seL4为底座的操作系统，为客户提供更高的业务性能，可靠性和安全性保障。

此外，鉴释所打造的高效的seL4特有工具链支持，从调试到性能分析等方面帮助开发者轻松开发出更高效的业务应用。