Advanced Software Engineering Techniques

Course 7 – 5 December 2023 Adrian Iftene [email protected] 1 } Recapitulation course 7 ◦ Runtime Verification ◦ Model Checking ◦ MOP } Runtime Verification ◦ Java MOP Examples ◦ Tools: MaC, J-LO } SOA ◦ Defin...

Course 7 – 5 December 2023 Adrian Iftene [email protected] 1 } Recapitulation course 7 ◦ Runtime Verification ◦ Model Checking ◦ MOP } Runtime Verification ◦ Java MOP Examples ◦ Tools: MaC, J-LO } SOA ◦ Definition ◦ Service, Service contract ◦ Principles ◦ Examples 2 } Verification: comprises all techniques for showing that a system satisfies its specification } Runtime Verification: Runtime verification deals with those techniques that allow checking whether a system under scrutiny satisfies or violates a given safety property } It aims to be lightweight verification technique complementing verification techniques such as model checking or testing 3  Specification Test input/schedule generation Dynamic Static analysis analysis Specification Runtime visualization learning verification Program input output 4 } Model Checking is an automatic technique for verifying finite-state reactive systems } An important class of model checking methods are specified using temporal logic formulas } Temporal logic – a formula is not true or false in a static way in a model 5 } The basic functionality of a monitor is to decide if the current execution satisfies a property } Online monitoring - involves using a monitor to check the current execution of a system } Offline monitoring - involves using a monitor for a finite set of executions recorded } Safety property captures a behavioral property related to the execution trace 6 Program Execution Observation/Abstraction Action Abstract Trace Verification Monitors M1 M2 M3 … Action Monitors verify abstract traces against desired properties; can be dynamically created or destroyed (Meredith, Roșu, 2010) 7 } The observation + the verification mechanisms } Example: for global property “always (x > y)” 8 1) On-line: http://fsl.cs.uiuc.edu/index.php/Special:JavaMOP3 9 import java.io.*; import java.util.*; suffix HasNext(Iterator i) { event hasnext before(Iterator i) : call(* Iterator.hasNext()) && target(i) {} event next before(Iterator i) : call(* Iterator.next()) && target(i) {} cfg : S -> next next @match { System.err.println("! hasNext not called before next"); __RESET; } } 10 package mop; import java.io.*; import java.util.*; import java.security.*; MsgDigest(MessageDigest P) { event getInstance after(MessageDigest P) : call(* MessageDigest.getInstance()) && target(P) {} event update after(MessageDigest P) : call(* MessageDigest.update()) && target(P) {} event reset before(MessageDigest P) : call(* MessageDigest.reset()) && target(P) {} event digest before(MessageDigest P) : call(* MessageDigest.digest()) && target(P) {} ere : getInstance update (update* reset* update* digest)* @fail { System.err.println("Problem in Message Digest has occurred!"); __RESET; } } 11 package mop; safe [ next -> start import java.io.*; hasnext -> safe import java.util.*; ] unsafe [ full-binding HasNext(Iterator i) { next -> unsafe event hasnext after(Iterator i) : hasnext -> safe call(* Iterator.hasNext()) && target(i) {} ] event next before(Iterator i) : call(* Iterator.next()) && target(i) {} alias match = unsafe fsm : start [ @match { next -> unsafe System.out.println("next called without hasNext!"); hasnext -> safe } ] } 12 SafeFileWriter(FileWriter f) { static int counter = 0; int writes = 0; event open after() returning(FileWriter f) : call(FileWriter.new(..)) {this.writes = 0;} event write before(FileWriter f) : call(* write(..)) && target(f) {this.writes ++;} event close after(FileWriter f) : call(* close(..)) && target(f) {} ltl : [](write => (not close S open)) @violation { System.out.println("write after close or file is not open"); } } 13 CipherOp(ASPECipher cipher, ASPEPoint point, PublicKey pKey) { event publicKeyLoad after(ASPECipher cipher, PublicKey pKey) : call(public void loadPublicKey(PublicKey) throws *Exception ) && args(pKey) && target (cipher) {System.err.println("MOP public key called");} event encrypt before(ASPECipher cipher, ASPEPoint point) : call( public ASPEPoint encrypt(ASPEPoint) throws *Exception ) && args(point) && target (cipher) {} ere : (publicKeyLoad encrypt)* @fail { System.err.println( "! loadPublicKey has not been called before calling encrypt!"); __RESET; } } CipherDecryptionOp(ASPECipher cipher, ASPEPoint point, PrivateKey pKey) { event privateKeyLoad after(ASPECipher cipher, PrivateKey pKey) : call(public void loadPrivateKey(PrivateKey) throws *Exception ) && args(pKey) && target (cipher) {} event decrypt before(ASPECipher cipher, ASPEPoint point) : call( public ASPEPoint decrypt(ASPEPoint) throws *Exception ) && args(point) && target (cipher) {} event clear after(ASPECipher cipher) : call(public void clear() ) && target(cipher) { } ere : (privateKeyLoad decrypt clear)* @fail { System.err.println( "! The sequence: load privatekey, decrypt, clear not caled in this fashion!"); __RESET; } } } DeLap, M., et al., “Is runtime verification applicable to cheat detection?”, Proc. ACM NetGames '04, pp. 134- 138, 2004 } The main idea: Game implementation bugs are extensively exploited by cheaters, especially in massively multiplayer games 16 } With JavaMaC runtime verification the authors show how they identify a transaction bug } Bodden, E.: J-LO, the Java Logical Observer - A tool for runtime-checking temporal assertions 17 } Designed at U. Penn since 1998 } Components: ◦ Architecture for run-time verification ◦ Languages for monitoring properties and trace abstraction ◦ Steering in response to alarms } Prototype implementation ◦ Implementation of checking algorithms ◦ Recognition of high-level events } For Java programs: automatic instrumentation 18 19 } PEDL (Primitive Event Definition Language) – abstraction } MEDL (Meta Event Definition Language) – abstract transformation } SADL (Steering Action Definition Language) – feedback 20 } J-LO, the Java Logical Observer, is a tool for runtime-checking temporal assertions in Java 5 applications (last version is from 2006) } Temporal properties can be specified using a linear time logic (LTL) over AspectJ pointcuts } Specification takes place right in the source code in the form of Java 5 annotations } The work is based on a Haskell-prototype 21 } At design time - The software architect should formulate temporal interdependencies (TID) between events in a formal way, best in LTL (linear temporal logic) } At implementation time - the programmers annotate their source code with LTL. They use J-LO as an additional tool in their build chain to instrument the application under test. } At testing time - the instrumented application will emit an error message whenever one of the temporal assertions is falsified or verified } At deployment time - J-LO is simply removed from the build chain 22 Syntax Arity Semantics X 1 LTL operator Next * F 1 LTL operator Finally G 1 LTL operator Globally U 2 LTL operator Until R 2 LTL operator Release ! 1 logical not && 2 logical and || 2 logical or -> 2 logical implies: f1 -> f2 = !f1 || f2 logical if and only if: f1 f2 = (f1 -> f2) && 2 (f2 -> f1) 23 } For each object of a type T, after a constructor has been called, its tearDown method is called before it is garbage collected and no method is called afterwards on this object (G – globally, F – finally) T t1, T t2: G( ( exit( call( T.new(..) ) ) returning t1 ) -> ( F( ( entry( call( * T.tearDown() ) && target(t2) && if( t1==t2 ) ) ) && ( G( !( entry( call( * T.*(..) ) && target(t2) && if( t1==t2 ) ) ) ) 24 ) } Recapitulation course 7 ◦ Runtime Verification ◦ Model Checking ◦ MOP } Runtime Verification ◦ Java MOP Examples ◦ Tools: MaC, J-LO } SOA ◦ Definition ◦ Service, Service contract ◦ Principles ◦ Examples 25 } SOA is a flexible set of design principles used during the phases of systems development and integration in computing } A deployed SOA-based architecture will provide a loosely-integrated suite of services that can be used within multiple business domains } SOA defines how to integrate widely disparate applications for a Web-based environment and uses multiple implementation platforms } JSON, XML are commonly used for interfacing with SOA services, though this is not required 26 } OASIS (Organization for the Advancement of Structured Information Standards ): A paradigm for organizing and utilizing distributed capabilities that may be under the control of different ownership domains } Thomas Erl: SOA represents an open, agile, extensible, federated, composable architecture comprised of autonomous, QoS-capable, vendor diverse, interoperable, discoverable, and potentially reusable services, implemented as Web services 27 } Service – a software component with following properties: ◦ Interoperability among different systems and programming languages ◦ is defined by an interface that is platform independent ◦ is accessible using a network ◦ operations defined in the interface will perform essential operations (“business functions”), aiming to achieve their business objects type ◦ a service interface and its implementation can be “decorated” with extensions that will make their presence felt at “runtime” 28 } Entity service - one or more “business” entities } Functional service - often does not have a representation in a business model, however, can be represented in a sequence diagram type. It is technology oriented and not for business (for example: logging and notification operations) } Process services - consists of a series of tasks (activities) related. These activities can be performed within the borders of a single business area, over several business areas or between organizations 29 } Generalization requires service analysis to determine it’s definition at concept level for the service } We can make an analogy with object-oriented programming, such an analysis in the context of OO type of relationship is called “is-a” } An exaggerated generalization can avoid capture relevant aspects of the service, decreasing the possibility of reuse, by this fact violates one of the basic principles of SOA 30 } Decomposition involves determining candidate elements to achieve a composition } Such an approach often leads to discovery services such entity or functional services, services that need to be separated } As a general principle, the more the service is better insolated, meaning lack of excessive interrelated, the more the service will be used/reused and eventually integrated into a scenario of “composition” 31 } Aggregation requires service analysis to determine the context to which it belongs, in the sense of interdependence relations } Items related to aggregation can be classified as existing processes, services or candidate services } We can also make a parallel with object-oriented programming, the process is called searching of “has- a” relations 32 } Applying the above principles is necessary for discovery of services that can be composed } Additional principles: ◦ Reuse ◦ Security ◦ Interoperability ◦ SLA (Service Level Agreements) ◦ Granularity ◦ Contract ◦ Process 33 } Reuse: the main goal of this technique is to provide a contract. Based on system analysis is aimed to identify the degree of reuse that we can have for this service } Security: usually this is taken into account at application level. When modeling the components that will provide security services will be placed in a general security model of SOA solutions that will include SAML (Security Assertion Markup Language), a “Policy Enforcement” transportation security specifications, digital signatures, Kerberos, etc. 34 } Interoperability: in the context of object-oriented programming, objects communicate only with other objects, for services this principle is not applied, the basic idea being that the communication between software components implemented on heterogeneous software platforms } SLA (Service Level Agreement): services must have defined contracts, “agreement” at service level. These types of specifications are very important because some service in an SOA context will be reused several times, in different contexts by different processes 35 } Granularity: a service often will be integrated into an environment where services are evolving in terms of interaction, therefore interoperability between different systems } Defining a good granularity (business specific features, there is not a high degree of interdependence) we guarantee reuse for that software component 36 } Contract: in a model (in the sense of SOA applications), the definition of a contract represents identification of necessary elements at global level } Some of the items will be referred as service attributes, and others will serve as metadata displayed in the context of WS-MetaDataExchange. Should be noted that often will be counted also non-functional elements, their declaration is usually facilitated by technology that supports SOA application development 37 } Process: analysis differs from traditional approaches (in terms of building systems able to deliver a clear set of features) focusing on object-oriented paradigm, their importance in the context of IT is given the opportunity to translate, to represent a business process as a web service (the latter developed by OASIS standard - WS-BPEL 2.0) } Many projects (technologies that enable software development) provides the solution for achieving orchestration mechanism (opposite concept of web services choreography more specifically classic – “WS- Choreography”) support for working with business processes and exposing them as services 38 } SOA separates functions into distinct units, or services, over a network in order to allow users to combine and reuse them in the production of applications } These services and their corresponding consumers communicate with each other by passing data in a well-defined, shared format, or by coordinating an activity between two or more services } Requires low coupling between services } SOA developers associate individual SOA objects by using orchestration (automated arrangement, coordination, and management) 39 } XML, JSON – to structure data } WSDL - describes the services } SOAP – communication protocol } Programmers develop services using Java, C, C++, C#, Visual Basic, COBOL, PHP 40 41 } A service contract needs to have the following components: } Header (Name + Version + Owner + Responsibility assignment (RACI) + Type) } Functional (Functional Requirement + Service Operations + Invocation) } Non-Functional (Security Constraints + Quality of Service + Transactional + Service Level Agreement + Semantics + Process) 42 43 44 45 46 47 } Monitor Model: http://fsl.cs.uiuc.edu/pubs/meredith-rosu-rv- 2010-slides.ppt } J-LO: http://www.sable.mcgill.ca/~ebodde/rv//JLO/index.html } SOA: http://en.wikipedia.org/wiki/Service-oriented_architecture } SOA Example 1: http://web.progress.com/en/esb-architecture- lifecycle-definition.html } SOA Example 2: http://download.oracle.com/docs/cd/E13156_01/ wloc/docs103/example/ex_service.html } SOA Example 3: http://ooxs- be.goracer.nl/EN/architecture/SOA.html } SOA Example 4: http://blogs.msdn.com/b/mmoin/archive/ 2006/10/09/soa-boot-camp.aspx } SOA Ionut Apetrei: http://thor.info.uaic.ro/~adiftene/Scoala/2011/TAIP/Courses/TAIP0 6.pdf 48 } Introduction to program monitoring: http://www.runtime- verification.org/course09/lecture1/lecture1.pdf } Patrick Meredith and Grigore Rosu. 2010. Runtime Verification with the RV System, First International Conference on Runtime Verification (RV'10), Springer, Lecture Notes in Computer Science, 6418, 136- 152 } DeLap, M., et al.: Is Runtime Verification Applicable to Cheat Detection? http://www.comp.nus.edu.sg/~bleong/hydra/related/delap04runtim e.pdf } Sokolsky, O.: Run-time verification, 2006, http://www.cis.upenn.edu/~alur/CIS673/mac.pdf 49