契約編程：API的形式化規范.pdf

《契約編程：API的形式化規范.pdf》由會員分享，可在線閱讀，更多相關《契約編程：API的形式化規范.pdf（20頁珍藏版）》請在三個皮匠報告上搜索。

1、 2024 Carnegie Mellon University1DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.2024 Carnegie Mellon UniversityDISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.JULY 9,2024Alex VeseySoftware

2、EngineerContract Programming:Formalizing APIs 2024 Carnegie Mellon University2DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.Document MarkingsCarnegie Mellon University 2024This material is based upon work funded and supported by the Department

3、 of Defense under Contract No.FA8702-15-D-0002 with Carnegie Mellon University for the operation of the Software Engineering Institute,a federally funded research and development center.References herein to any specific entity,product,process,or service by trade name,trade mark,manufacturer,or other

4、wise,does not necessarily constitute or imply its endorsement,recommendation,or favoring by Carnegie Mellon University or its Software Engineering Institute nor of Carnegie Mellon University-Software Engineering Institute by any such named or represented entity.NO WARRANTY.THIS CARNEGIE MELLON UNIVE

5、RSITY AND SOFTWARE ENGINEERING INSTITUTE MATERIAL IS FURNISHED ON AN AS-IS BASIS.CARNEGIE MELLON UNIVERSITY MAKES NO WARRANTIES OF ANY KIND,EITHER EXPRESSED OR IMPLIED,AS TO ANY MATTER INCLUDING,BUT NOT LIMITED TO,WARRANTY OF FITNESS FOR PURPOSE OR MERCHANTABILITY,EXCLUSIVITY,OR RESULTS OBTAINED FRO

6、M USE OF THE MATERIAL.CARNEGIE MELLON UNIVERSITY DOES NOT MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT,TRADEMARK,OR COPYRIGHT INFRINGEMENT.DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.Please see Copyright notice for non-U

7、S Government use and distribution.This material may be reproduced in its entirety,without modification,and freely distributed in written or electronic form without requesting formal permission.Permission is required for any other use.Requests for permission should be directed to the Software Enginee

8、ring Institute at permissionsei.cmu.edu.2024 Carnegie Mellon University3DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.Example APIs and Contracts Contract Programming Implications for Security Getting StartedAgendaHow to make code more boringle

9、ss surprising 2024 Carnegie Mellon University4DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.Examples of functions with ill-specified contracts 2024 Carnegie Mellon University5DISTRIBUTION STATEMENT A This material has been approved for public

10、release and unlimited distribution.Examples of functions with ill-specified contracts 2024 Carnegie Mellon University6DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.Examples of functions with ill-specified contracts 2024 Carnegie Mellon Univers

11、ity7DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.Examples of functions with ill-specified contracts 2024 Carnegie Mellon University8DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.Applica

12、tion Programming Interface(API)“A set of functionalities independent of their implementation,allowing the implementation to vary without compromising the users of the component.”Joshua BlochA way to decouple what code can do for a user from how the code does it.2024 Carnegie Mellon University9DISTRI

13、BUTION STATEMENT A This material has been approved for public release and unlimited distribution.Mental ModelsWith abstraction comes a“mental”model and ambiguity“All models are wrong”George Box 2024 Carnegie Mellon University10DISTRIBUTION STATEMENT A This material has been approved for public relea

14、se and unlimited distribution.Contracts in Computer Science“A contract is a formal interface specification for a software component such as a function or a class”C+SG21(Contracts)Document P2900R3When a piece of code executes it will change the state of the computer system.For a precondition P,postco

15、ndition Q and command C it can be said that if P is true and C is executed then Q will be true(if C terminates).x+1=42 y=x+1 y=42 2024 Carnegie Mellon University11DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.Contracts:Conditions and Invariant

16、sContracts typically consist of:A set of preconditions that must be trueA set of post conditions the function guarantees will be trueA set of invariants that the function will not change 2024 Carnegie Mellon University12DISTRIBUTION STATEMENT A This material has been approved for public release and

17、unlimited distribution.Narrow and Wide Contracts“Wide”contracts have no pre-conditions“Narrow”contracts have(sometimes many)preconditionsExample:std:vector:size()WideNo-throw guaranteeExample:std:vector:at()NarrowMay throw and exception 2024 Carnegie Mellon University13DISTRIBUTION STATEMENT A This

18、material has been approved for public release and unlimited distribution.Contract Programming and SecurityResearch123has shown that bad APIs are bad for securityIncorrect usage of security functionsAssumed or implied preconditions or post conditionsInvariants that are notDont trust that developers w

19、ill read your documentationYour documentation may not serve their learning style4They might read it,but are likely to go to stack overflow too51 https:/dl.acm.org/doi/10.1145/2508859.25166552 https:/www.usenix.org/system/files/sec20-tang.pdf3 https:/dl.acm.org/doi/10.1145/28965874 https:/ https:/sur

20、vey.stackoverflow.co/2023/#learning-to-code-learn-code 2024 Carnegie Mellon University14DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.APIs and CWEsThere are many Common Weakness Enumerations pertaining to APIs Implementing:CWE 1059 “The produc

21、t does not contain sufficient technical or engineering documentation”CWE 628 “The product calls a function,procedure,or routine with arguments that are not correctly specified”Consuming:CWE 648 “The product does not conform to the API requirements for a function call that requires extra privileges”C

22、WE 475 “The behavior of this function is undefined unless its control parameter is set to a specific value”2024 Carnegie Mellon University15DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.Security Example:HeartbleedAssumptions:(1)pl is valid and

23、 points to the beginning of the payload,(2)the size of the payload should be the same as the value in the payload length field 2024 Carnegie Mellon University16DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.Security Example:HeartbleedWould a co

24、ntract have solved the issue?Maybe 2024 Carnegie Mellon University17DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.Getting StartedExisting codebasesStart with comments about assumptions,preconditions and post conditionsEnforcement through gradu

25、al typing if the language allowsGreen field projectsOpenAPI with definitions of parameters,responses and schemasLibraries like Guava(Java)and Preconditions in the Kotlin stdlibComing soon:Language support for contracts is expected in C+26(maybe)2024 Carnegie Mellon University18DISTRIBUTION STATEMENT

26、 A This material has been approved for public release and unlimited distribution.Levels of Contract FormalityCommentsDocumentationOpenAPI 2024 Carnegie Mellon University19DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.Levels of Contract Formali

27、tyRun time AssertionsCompile Time Assertions 2024 Carnegie Mellon University20DISTRIBUTION STATEMENT A This material has been approved for public release and unlimited distribution.Closing ThoughtsAPIs are useful and pervasive.Contracts help build better APIsPoorly defined APIs are a security riskThe formality of an API Contract is flexible