3-12543-Using SAST tool in safety and security application.pdf

1、1 2023 The MathWorks,Inc.Using SAST tool in safety and security application to accelerate development speed&improve robustLehua HuApplication Engineering/Polyspace Products MathWorks China2内容提要高完整性系统的特点为什么需要形式化验证将形式化验证用于软件研制流程 编码时即验证代码 提交前全面验证 集成到CI，加速验证3高安全高完整性系统高安全高完整性系统Definition:cf.Buncefield In

2、vestigation Glossary www.buncefieldinvestigation.gov.uk/glossary.htm严苛的行业认证标准高可靠和高容错设计严格的可追述和文档化正确性和完整性全面和复杂的验证和质保流程MATLAB Automotive Conference,Stuttgart,2015“When I step into a new car these days,I dont smell leather anymore,I smell software.”45失败的代价$7,500,000,000阿丽亚娜5号火箭:数据溢出星箭炸毁6设计空间测试测试*设计空间形式化

3、验证形式化验证(实际使用情形)设计空间形式化验证形式化验证(理想使用情形)测试无法保证软件质量7“Given that we cannot really show there are no more errors in the program,when do we stop testing?”Brent Hailpern,Head of Computer ScienceDijstra,“Notes on Structured Programming”(1972)Hailern,Santhanam,“Software Debugging,Testing,and Verification”,IBM

4、 Systems Journal,(2002)Program Testing“Program testing can be used to show the presence of bugs,but never to show their absence”Edsger Dijkstra,Computer Science Pioneer程序测试可以显示软件问题的存在，但永远无法显示其不存在。程序测试可以显示软件问题的存在，但永远无法显示其不存在。既然我们无法知道程序中还有没有问题，那我们何时该停止测试？既然我们无法知道程序中还有没有问题，那我们何时该停止测试？8Increasing Softwa

5、re Size&ComplexityMillions of lines of codeBillions of runtime modes and statesToo much to verify using manual review and testing practices.People lack speed,attention span,and make mistakes.开发高质量软件越来越有挑战性Evolving Software Development Processese.g.DO-178,ISO 26262,ISO 21434,MISRA,AUTOSAR,CERT,Thousa

6、nds of rules to understand,follow,and document with every code change.New rules and standards each year.e.g.,CI/CD,DevOps,DevSecOps,Software FactoryDemand speed,scale,consistency,repeatability hundreds of time per day.Daily SW releases and OTA updates.Emerging Coding,Safety&Security Standards9软件质量铁三