新興技術：軟件行為計算在安全性與正確性中的應用.pdf

1、The Emerging Technology of Software Behavior Computation for Security and CorrectnessRick LingerAssuranceLabs Inc.1Copyright 2024 AssuranceLabsrick.lingerassurancelabs.tech202-701-6257SEI 2024 Secure Software By Design ConferenceSoftware Can Dwarf Hardware in Complex Systems2Cost allocation Since th

2、e 1980s,HW/SW cost ratio has shifted from 10:1 to 1:2Parts countF-35:8M SW parts(instructions),300K HW parts:Ratio 27/1NASA:“We are no longer building hardware into which we install enabling software,we are building software systems which we wrap up in enabling hardware.”*Dr.Patricia Sanders,Chair,A

3、erospace Safety Advisory Panel,testifying at House hearing“Keeping Our Sights on Mars,”May 8,2019.Copyright 2024 AssuranceLabsHard Work and Mega-Failures Every effort is made to ensure correctness and security But failures continue to occur,with serious consequences:Boeing:Starliner spacecraft failu

4、re to achieve orbit:Multiple$100M CrowdStrike:Global IT meltdown:May be multiple$100BConsortium for Information and Software Quality:2022 cost of poor software in US:$2.41T*Copyright 2024 AssuranceLabs*Krasner,H.,“The Cost of Poor Software Quality in the US:A 2022 Report,”Dec.2022,https:/www.it-cisq

5、.org/the-cost-of-poor-quality-software-in-the-us-a-2022-report/Limitations of Todays MethodsTestingPrincipal means of software assurance.Can show the presence of errors not their absence.Can exercise only a small fraction of possible executions.Static AnalysisMust unroll loops,cannot determine full

6、loop functionality.Reviews Subject to human fallibility.Copyright 2024 AssuranceLabsFormal MethodsEffective,but slow and costly.All vital and useful,but can we do better?A New Approach:Computing the Behavior of Software5Function Extraction(FX)Technology An emerging mathematics-based technology Compu

7、tations reveal all possible behaviors of software Computations are full domain-to-range no behavior is left outA single FX behavior computation 1)Subsumes all possible test cases2)Shows how results are computed3)Enables verification and security analysisCopyright 2024 AssuranceLabsBreakthroughloop b

8、ehaviorcomputationTwo 75-Year Problems:Specification and VerificationCopyright 2024 AssuranceLabs FX computes as-built functional specifications:No specification writing for users FX computes full behavior for verification:No learning verification methods for users Source CodeFunction Extraction(FX)

9、Computes Code BehaviorComputedBehaviorAs-built specificationFull behavior for verificationMalicious content cant hideAny C-like languageAny originMathematical precisionNo testing,no executionDomain KnowledgeEquation SolverInvariant RelationsMathematicaFX Origin:Cleanroom Software Engineering Process

10、*7 Objective:Near zero-defect software with certified reliability(same as SSBD)Principles:Rigorous development,no debugging,statistical usage-based testing Process:Copyright 2024 AssuranceLabsCleanroom DevelopmentPractical development and verification methods to approach zero defects prior to first

11、execution.Cleanroom TestingRepurpose testing from endless debugging to statistical certification of fitness for use.Behavior ComputationSupports Cleanroomcorrectness verificationMany other use-cases across the life cycle*Linger,R.and Trammell,C.,Technical Report CMU/SEI-96-TR-022 ESC-TR-96-022:Clean

12、room Software Engineering Reference Model Version 1.0,Nov 1996.Near zero-defect codeA Purposely Complex Illustration of Behavior ComputationCopyright 2024 AssuranceLabs Function calls,nested loops Free of semantic clues What does the program do?(ji)The Behavior Computed by FXCopyright 2024 Assurance

13、Labs Program has two cases of behavior Final state in terms of initial state Domain-to-range mapping Shows how final values are computed Computed by an FX prototypeConditional Concurrent Assignments(CCAs)are the canonical form for behavior expression:“P”for prime the final value.Program does not ter

14、minate for (i!=j|j 0)|i=divisor)n:=n divisor;/remainder function for positive n and positive divisorpublic static void remainder(int n,int divisor,int c)if c=3567214837 n=9;else while(n=divisor)n:=n divisor;FX computation shows malicious functionality:Case 1:n=divisor and c/=3567214837 n=n mod divis

15、or Case 2:c=356721483 n=9FX computation shows correct functionality:Case 1:n=divisor n=n mod divisorA Proportional,Integral,Derivative(PID)Controller11Used for real-time control in DoD systems,elsewhereReads sensors,computes status,commands actuatorsImagine controlling temperature in a space habitat

16、Copyright 2024 AssuranceLabsComputed Behavior of the PID Controller12Proportional termIntegral termDifferential termBehavior computation shows how values are computed Testing shows only final valuesCopyright 2024 AssuranceLabsScaling Up Behavior Computation13Compute and propagate behavior up the hei

17、rarchy:Copyright 2024 AssuranceLabsPgm APgm BPgm CPgm DPgm EProgramHierarchyPgm APgm BFn CPgm DFn ELeaf NodeComputationsPgm AFn BFn DIntermediate NodeComputationsFn AFull ProgramBehaviorFX and AI-Code GenerationCopyright 2024 AssuranceLabsLLM CodeGenerationLLM-Generated CodeIterative Specification:U

18、ser analyzes code and tests and defines a revised query,until the code is satisfactoryInitial Specification:User creates LLM code generation queryRequirementsUserInspect,Test the CodeEmpiricalProcessAI-Code Generation with Computed BehaviorCopyright 2024 AssuranceLabsFunction Extraction(FX)Computes

19、Code BehaviorComputed Behavior:User analyzes behavior,finished if satisfactoryComputedBehaviorIterative Code Modificationand Verification:User modifies code using function operators untilbehavior is satisfactoryFX provides Assume,Capture,Verify,and Establish operators for interactive user modificati

20、on and verification of codeLLM CodeGenerationIterative Specification:User analyzes behavior and defines a revised query until the behavior is satisfactoryInitial Specification:User creates LLM code generation queryRequirementsUserDefinitiveProcess DefinitiveProcess LLM-Generated CodeAn Educational A

21、pplication Software engineering is the only discipline that teaches how to create artifacts,and only later,if at all,teaches how to verify them.Aeronautical engineering doesnt teach how to design airplanes,and then verify by flying with passengers.Civil engineering doesnt teach how to design bridges

22、,and then verify by driving over them.Behavior computation can help combine development and verification into a single educational process.Copyright 2024 AssuranceLabsGetting Operational with FX Proof-of-Theory prototype exists.Proof-of-Implementation prototype underway,full system next.Management payoff is competitive advantage through reduced risk,improved quality and security.Educational payoff is more effective hires who canverify their code.Partners and pilot projects are welcome.Copyright 2024 AssuranceLabs