博客

鉴释及合作伙伴进迭时空受邀在德国慕尼黑开幕的seL4峰会上发表演讲。分享了鉴释在分析seL4内核代码覆盖率方面的工作。同时介绍测量结果和提高代码覆盖率的方法。 文末附PPT下载方式。

在峰会上，我们主要分享了如何让seL4符合ISO 26262标准的方法和进展。

​随着seL4进入汽车应用，拥有行业标准将是大规模采用的一个重要步骤。ISO 26262 ASIL-D是众所周知的汽车软件供应链的关键标准。而MISRA C标准很适合使C语言编写的软件符合ISO 26262 ASIL-D标准。

在谈到合规性问题时，通过MISRA合规性的分析，不难发现存在一系列与工具冲突的问题。我们要如何解决这些问题。我们是否要修复它？如果我们不改变它，认证机构是否接受？鉴释CEO梁宇宁指出在MISRA中，当你看到两个定义，要么是变量规则定义，要么是结构定义，它们是冲突的。有两种方法可以解决这个问题。要么改变你的变量，要么改变你的stock。那么，我们要如何选择呢？通过反复论证，我们发现改变变量或许是一个比较好的解决方式。

演讲尾声，有观众提问：“为什么行业还停留在半个世纪前的软件安全的编码规则检查，而不是使用形式化验证这种更可靠的方法？”。我们认为这跟汽车行业繁杂的供应链有关。当这个行业仍然处于大规模生产时，完全废除现有标准采用全新的东西是非常困难的。因此，一个更切实际的方法是使seL4符合ISO 26262标准，作为工业化量产的第一步。

最后，我们希望我们的工具可以帮助seL4被汽车行业厂商采纳和接受，并期待在将来看到它被广泛地应用在更多领域。

点击此处下载演讲全文（演讲为英文）。