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軟件質量鐵三

7、角&限制和風險QualityScope(features)CostTimeConstraints:The Project Management“Iron Triangle”“Pick any 2”Health,Safety of CustomersCost of recalls/repairs,legal liabilityDamage to ReputationCompetitive Advantage,Market Share10The power of code proving11xyy=x+Plot of all possible values for xand y什么是抽象解釋法?驗

8、證 y=x/(x-y)的除零12xyy=x+類型分析ijkl什么是抽象解釋法?驗證 y=x/(x-y)的除零13xyy=x+無需測試用例 無需執行代碼 靜態分析抽象演繹法什么是抽象解釋法?驗證 y=x/(x-y)的除零14理解抽象解釋法原理signed char x,y;x=random_char();if(x 0)else if(x!=0)else printf(“%d”,x);-128127112711275-128-15y=100/(x+1);y=100/(x+1);y=100/(x+1);x=5;x=5;?y=200/x;y=200/x;-128-2-128-2015理解抽象解釋原理1

9、7理解抽象解釋原理所有可能路徑所有可能輸入所有操作運算183月后6月后T0軟件的改進，但無確切的可衡量的證明。一般靜態分析只能說明有問題，不能說明沒問題。不能用于證明代碼正確性。.安全證明0%安全證明可行、可度量Code Prover 有何獨到之處？19形式化證明缺陷&漏洞檢查編碼規范、信息安全指南代碼度量Code ProverFully Trusted ComponentsReliable,Robust,Safe,SecureProven free of critical runtime defects and vulnerabilitiesAdditional credits for st

10、andards.完整的靜態分析解決方案Bug FinderHigh Quality,Secure,Compliant CodeMeasurable,Maintainable,ConsistentVery few defects or vulnerabilitiesCredits for functional safety,cybersecurity standards.20高效使用形式化分析到開發流程中高效使用形式化分析到開發流程中Collaborate with Team MembersCatch and fix bugs while you codeAutomate with CI Wor

11、kflowsMonitoring with DashboardAnalysis before submit21編碼時即檢測和修復缺陷在IDE中編碼的早期發現問題安全隱患常見缺陷和漏洞、編碼規范等支持Eclipse、VS 和 VS Code提供與代碼編輯器和IDE的集成API22第一時間修復軟件缺陷on demand.before committing.before running tests.while you remember the code.when its easiest.when its least expensive.Also supported:and custom integr

12、ations+Help develop good habitsDefectsCoding rulesNaming rulesCert/CWEGuidelines23編碼時即檢測和修復缺陷24RequirementsCodingIntegrationTestingAcceptanceTestingProductionLeft shift your verification with PaYC1x5x10 x30 x15xSource:National Institute of Standards and Technology(NIST)25提交版本前分析No process involvedRe

13、duce reworkNo tech debtrepair with low cost26使用桌面版擴大更多驗證聲明不匹配修飾符不匹配類型別名沖突死鎖/重復鎖等運行時錯誤證明上溢/下溢除零數組越界緩存Out of boundary緩存訪問越界非法指針解引并發訪問沒有運行時錯誤遠比零漏洞重要27快速修正代碼問題所在準確位置問題追蹤范圍信息28交付安全的軟件單元實際調用是分析的特例29信息流和共享變量訪問證明綠色綠色:安全可靠安全可靠共享內存訪問安全橙色橙色:未被證明未被證明共享內存的訪問可能不安全共享內存的訪問可能不安全變量范圍變量范圍變量在程序中所有位置的變量任務和中斷任務和中斷對共享內存的讀

14、寫操作對共享內存的讀寫操作30提供審查依據MISRAViolationNo loss of sign or value31集成Polyspace到您的CI工作流中32運用看板監控軟件質量33運用看板監控軟件質量34團隊協同評審35團隊協同評審36Comprehensive static analysis integrated in your environmentBuildQualityGateAnalyze CodePolyspace Bug Finder ServerPolyspace Code Prover ServerPolyspace AccessTestCodeRepository

15、TestPolyspace as You Code*DeveloperReview Results/CollaborateIDEQuality MonitoringTeamReviewBuildComponent&other local workflowsContinuous Integration automations*Polyspace as You Code is a feature of Polyspace Access37Thank you!38Change the world byAccelerating the Paceof discovery,innovation,development,and learningin Engineering and Science