Model. and analysis of information. systems. V.15, 3 (2008) UDC Development of Correct Java Card Programs Based on the Automata Approach Klebanov A.A., Shalyto A.A. aimed at generating correct Java Card code. In this case, the code is generated from a high-level description based on the technology of automatic programming. An additional advantage of this approach is the ability to generate a formal application specification. The conformity of the source or byte code to the specification can be checked by various verifiers or by means of dynamic or static checking. KEY WORDS: automaton, automaton programming, model, verification, model checking 1. Introduction A smart card [1] is a plastic card with a built-in chip and memory to store and process information. In fact, smart cards are tamper-proof computers the size of a credit card. In addition to being protected, these cards have such advantages as mobility and ease of use. They provide information storage, authentication, are used in payment systems, mobile communications, etc. Java Card technology [1] adapts the Java platform for use on smart cards. In addition to the advantages inherent in Java technology (security, reliability, support for the principles of object-oriented programming, cross-platform, etc.), when using the technology in question, firstly, The development process is greatly simplified (the Java Card platform allows the programmer to abstract from the internal features of cards of each specific manufacturer), and secondly, a mechanism for launching several applications on one card is introduced. The Java Card API is a superset of a subset of the Java API. This means that Java Card lacks support for multithreading, strings, multidimensional arrays, garbage collection, and so on due to limited card resources. However, the Java Card API has been extended with additional functionality necessary to solve the problems that arise when using smart cards. This extension includes sending and receiving special commands (Application Protocol Data Unit, (APDU) commands), working with PIN codes, cryptographic algorithms, and so on. Note that Java Card applications are usually called applets. To maintain logical integrity, some aspects of the Java Card technology will be described in more detail in those parts of the work where it is necessary for understanding. Formal Methods are mathematically rigorous methods and tools for the specification, design, and verification of software and hardware [2]. Similar to automata programming [3], their application in software engineering is based on the popular idea of using reliable and proven technologies from other engineering disciplines. The general purpose of using formal methods is to create robust software and hardware. There are a number of reasons [4] why Java Card technology is interesting for researchers in the field of formal methods. First, Java Card applications are very security and reliability critical. which is explained by the specifics of the fields of application of smart cards, in which the cost of an error is very high. Secondly, Java Card is the most widely used Java platform in the world, as smart cards are issued in huge numbers. Therefore, unlike software for personal computers, update or fix applications for already.
Modeling and analysis of information systems V.15, 3 (2008) issued maps can be quite laborious and economically unprofitable. And finally, the limited resources and less functionality of the Java Card compared to Java technology ensures that programs do not have too complex behavior and a large number of control states [3]. Java Card applications can become a good training ground for various formal methods, on the one hand, the programs in this case are quite simple, and on the other hand, they are of specific practical interest, and not artificially created toy code. Thus, the task of applying formal methods for designing and verifying Java Card applications seems to be relevant and realizable. The purpose of this work is to expand the technology of automata programming to create correct Java Card programs. At the same time, it is necessary to solve a number of problems related to the implementation of the possibility of generating the skeleton of the source code of Java Card applications and their subsequent verification at the level of the source and byte codes. 2. Analysis of existing works It follows from the above that the analysis of existing works can be carried out in two directions, one of which is the generation of Java Card-code from high-level specifications, and the second is the verification of automatic programs. Generation of Java Card-code from high-level specifications There are two research projects, aimed at generating Java Card code from high-level specifications. The first of them [5] is based on the domain-specific language SmartSlang, which allows you to describe programs using high-level constructs typical of smart cards. However, it does not use an automaton approach, and therefore the project has little to do with the real work. The second project is considered in works [6, 7]. In these studies, the code is generated based on the state machine describing the applet. In [6], a verifier is used as an editor for finite state machines, and in [7], UML is used to describe automata. This work has several advantages over these studies. First, the technology of automata programming is used, which assumes the description of behavior by a hierarchical system of automata, and not just one automaton, as in [6, 7]. In [6], the question of modeling the host application itself and its interaction with a smartcard remains open. Allocating the host application as a separate event provider within the automaton approach sufficiently solves this issue. The notation used in automata programming technology hides the low-level features of the Java Card language, which facilitates the process of developing programs and increases their reliability. Indeed, the programmer is offered to operate not with byte arrays, but with short identifiers, for which a text description is always available. Second, the proposed approach generates a more complete specification. In particular, under certain restrictions, it is possible to generate preconditions for methods that are called upon entering a state. In [6], this question is referred to as open. Finally, a number of plugins have been developed for the UniMod tool [8], allowing verification of the automaton model [9]. Note that in [6] the verifier is used exclusively as a graphical editor for creating automata, and its use for its intended purpose is mentioned only in the section describing further studies. However, in a later work [7], model verification is not mentioned at all. Moreover, the issue of code generation is considered to be of secondary importance, and extracting an automaton model from the source code is considered an attractive task, which is opposite to the goal of this work. The most typical example of dynamic verification is testing. The essence of this method is to test the functionality of the program using some examples. Despite the widespread prevalence of this approach, it has a significant drawback of dependence on a specific scenario. It is well known (E. Dijkstra) that testing cannot prove the absence of errors in a program.
Development of Correct Java Card Programs Based on the Automata Approach 49 In this paper, the issue of application verification is considered as a matter of static verification, which includes Model checking technologies [10] and theorem proving [11]. When using the automaton approach, the Model checking technology plays a key role [10, 12, 13]. It allows you to automatically check whether a given requirement, expressed in the language of temporal logic, is fulfilled on the behavior model of a system with a finite number of states. Roughly speaking, the check is carried out using a search over the entire set of states, and the finiteness of the model ensures that the search will eventually complete. It is obvious that for general programs the use of this technology is very problematic. The model for verification has to be built heuristically. This raises the question of how adequate the resulting model is to the original program. However, Model checking is ideal for verifying automata programs. Indeed, this technology presupposes the formal construction of a model according to the program, which is a special kind of finite state machine. Therefore, the process of constructing a model from an automaton program can be automated, and, as a consequence, errors caused by the discrepancy between the model and the program will disappear. The writing of formal requirements for automaton programs is traditionally also simplified in comparison with constructed ones, since for this class of programs the semantic gap between the requirements for the program and the requirements for the model is practically eliminated in the course of constructing the automata. If an error occurs, a counterexample is issued; its translation into an automaton program can also be performed automatically. The disadvantage of Model checking technology as applied to automatic programming is that it covers only the logical part of the program. For the present work, another technology of verification, the method of proving theorems, is also important. Within the framework of this technology, both the system itself and the requirements for it are expressed using formulas of mathematical logic. Logic is defined by a set of axioms and inference rules, and the verification process consists in proving certain requirements. Unlike Model checking technology, theorem proving can be performed in the case of an infinite-dimensional state space. The disadvantage of this technology is the presence of non-existent error messages, often indicating a problem in the proof system, and not in the program itself. Model checking technology does not have this disadvantage. It is logical to raise the question of the possibility of combining these two technologies in such a way as to compensate for the shortcomings of each of them. Possible solutions are presented in a number of works. In work [14], devoted to the current state and prospects of formal methods, there is a remark that for the description and analysis of a complex system, most likely, it will not be enough to use only one formal method. Therefore, it becomes important to combine them. The main focus in this area is considered to be a combination of model checking and theorem proving technologies. Two approaches are proposed, firstly, to use Model checking as a decision-making tool for proving theorems, and secondly, using theorem proofs to obtain models in the form of finite automata and apply model checking to them. This work uses a different approach, which will be described in detail below. Its essence is that at different stages of the development and implementation of the application, it is proposed to apply various verification methods that are relevant for the current stage. In this case, it is possible to combine model verification with verification of its implementation, including verification of the byte code. Note that in [12] it is also stated that verification by the theorem-proving method is applicable to automatic programs. At the same time, however, it is argued that this approach is very laborious and useless for testing the logic of the program, and can only be used to test the input and output actions. In this work, an attempt is made to refute the first part of the statement (the second part is fully confirmed), firstly, a method for checking the program logic is described, and secondly, provides an overview of the tools (already existing and created within the framework of this work) that implement this check with a high degree of automation. 3. Methods and technologies used Before presenting the main part of the work, let us describe some of the methods and technologies on which it is based. The contract design methodology [15, 16] is used to develop reliable software. It proposes to consider the constituent parts of programs as the implementation of some formal specification, and not just as executable code. The main idea of this methodology is that the class and its clients enter into a contract with each other. The client must ensure that certain conditions are met before calling the class. For this, the class undertakes to fulfill implementing this check with a high degree of automation. 3. Methods and technologies used Before presenting the main part of the work, let us describe some of the methods and technologies on which it is based. The contract design methodology [15, 16] is used to develop reliable software. It proposes to consider the constituent parts of programs as the implementation of some formal specification, and not just as executable code. The main idea of this methodology is that the class and its clients enter into a contract with each other. The client must ensure that certain conditions are met before calling the class. For this, the class undertakes to fulfill implementing this check with a high degree of automation. 3. Methods and technologies used Before presenting the main part of the work, let us describe some of the methods and technologies on which it is based. The contract design methodology [15, 16] is used to develop reliable software. It proposes to consider the constituent parts of programs as the implementation of some formal specification, and not just as executable code. The main idea of this methodology is that the class and its clients enter into a contract with each other. The client must ensure that certain conditions are met before calling the class. For this, the class undertakes to fulfill The contract design methodology [15, 16] is used to develop reliable software. It proposes to consider the constituent parts of programs as the implementation of some formal specification, and not just as executable code. The main idea of this methodology is that the class and its clients enter into a contract with each other. The client must ensure that certain conditions are met before calling the class. For this, the class undertakes to fulfill The contract design methodology [15, 16] is used to develop reliable software. It proposes to consider the constituent parts of programs as the implementation of some formal specification, and not just as executable code. The main idea of this methodology is that the class and its clients enter into a contract with each other. The client must ensure that certain conditions are met before calling the class. For this, the class undertakes to fulfill The client must ensure that certain conditions are met before calling the class. For this, the class undertakes to fulfill The client must ensure that certain conditions are met before calling the class. For this, the class undertakes to fulfill
Modeling and analysis of information systems V.15, 3 (2008) other conditions after the completion of their work. The main advantage of the described methodology is the enforceability of contracts, the compiler translates them along with the source code. Therefore, any breach of contract during program execution can be detected immediately. Java Modeling Language (JML) [17] is a language for specifying Java modules (interfaces and classes) that describes both behavior and signature. JML is based on design-by-contract ideas and model-based specifications. The key elements of any specification are requires, ensures, and invariant. In the JML language there is an expression \ old (e) borrowed from Eiffel (a programming language developed to support design technology by contract [15]), which is equivalent to the value of expression E at the time of entering the body of the method. Changes to the value of a variable can be constrained using the constraint keyword, \ old () expression, and logical constructs such as a ==> b (implication) or a <==> b (equivalence). BOMs are written between or after. Thus, the standard Java compiler treats them as comments and simply ignores them. They are processed by specially developed means. To support JML, a large number of tools have been developed with different functionality [18]. The simplest way to check for code compliance with a specification is a runtime check, the JML compiler (jmlc) runs the annotated Java code and dynamically checks for type conformance and specification violations. Static verification (ESC / Java2) and formal verification (KeY, Loop, JACK) do not require launching the application and are able to solve much more complex problems, but with the help of the user and at the cost of some assumptions. Despite the fact that JML can be used to annotate arbitrary Java applications, at the moment the Java Card is considered the main area of its application [18]. 4. Statement of the problem and the scheme of the proposed solution Solving the problem of creating correct Java Card programs within the framework of using the automaton approach requires solving a number of subtasks: 1. Expand the existing technologies for generating code to obtain the possibility of creating a skeleton of Java Card applications from their automaton description. 2. Develop a method that allows you to generate a formal annotation to the code, covering the largest number of properties of the original automaton model. 3. Investigate existing tools for working with the JML language in order to identify suitable for solving diverse problems associated with the verification of annotated code. The general scheme of the proposed approach is shown in Fig. 1. It is proposed to solve the problem in several stages. On the first of them, a skeleton of the source code is generated from the automaton model, which describes the application logic with stubs for methods that implement input and output actions (solution of subproblem 1). In addition, a formal specification of the application in the JML language is generated (solution of subproblem 2). Then the input and output methods are manually implemented and, possibly, the application specification (JML annotation) is supplemented. Finally, using special tools, the compliance of the source code or byte code with the specification is checked (solution of subproblem 3). In this case, warnings about possible errors are issued to the user. 5. Automated approach for creating and verifying applications for smart cards In [19], it is proposed to divide systems into transforming and reactive systems. The transforming system processes the input information and issues a response based on it. The reactive system must constantly react to incoming influences. At the same time, it does not calculate any specific function, but maintains interaction with the environment. The reactive system stores its current internal state, and its response to the environment and state change are completely dependent on the input action and the current state. In this work, we use the automata programming proposed in [3, 20]. It is a kind of synchronous programming [21],
Development of Correct Java Card Programs Based on the Automaton Approach 51 Fig. 1. Scheme of the proposed approach According to the automaton programming paradigm [22], the program is considered as a system of automated control objects. At the same time, the program contains event providers, a control system consisting of interacting state machines, and control objects. Consider the features of the Java Card platform as a reactive system [19]. Interaction with a smartcard is carried out using card readers [1]. This device supplies power to the card and creates a communication channel between the card and the computer or terminal on which the host application is installed. The communication channel is half-duplex and uses the master-slave model. The smart card is always the slave and the host application is always the master. It means, that the smart card is always waiting for a command from the host application. The sequence of commands comes from the host application through the card reader in the Java Card Runtime Environment (JCRE). The commands are then passed to the selected applet. The applet processes the command and sends a response in the opposite direction. Thus, the interaction between the host application and the smart card can be interpreted as event-driven. Since the event providers of the host application and the smart card control object can be isolated, automatic programming can be effectively used to create robust Java Card programs (Figure 2). Rice. 2. Interpretation of automatic programming for the Java Card platform Application of the automatic approach does not free the programmer from writing code, since only that part of the functionality is generated that implements the logic of the system.
Modeling and analysis of information systems V.15, 3 (2008) manual creation of a code that implements input and output actions. The problem lies in the lack of means for checking the compliance of the code with its model and checking the methods that implement the input and output actions. The suggested way out of this situation is the use of contracts. Contracts also describe how different parts of a program interact, but they do so at a lower level of abstraction. If, along with the generation of the source code, a specification isomorphic to the model is generated, then, despite the lowering of the level of abstraction, the possibility of verification will remain. Therefore, the use of JML allows us to bridge the gap between the model and the specific implementation. Thus, it is possible to avoid the situation when the limited model causes unexpected errors in the program, or vice versa, errors in a poorly constructed model will signal non-existent errors in the program. In the case of verification of applications using JML, there is no need to build a formal model, the annotated source code itself is fed to the input of the verifier. As noted above, Model checking technology is limited only to checking the application logic, which is its main drawback. The generated code annotations allow you to accomplish similar tasks. However, if you add them manually, you can check a much larger amount of program properties, such as, for example, the behavior of methods that implement input and output actions, their interconnection, errors common in programming, such as an array index out of range, access to a nonexistent place in memory and much more. 6. Code and Specification Generation (Practical Implementation) All Java Card applets have a standard structure - they must override the methods of the base Applet class. To clarify the code generation process, we briefly describe [1] each of these methods in the order in which they are called by the JCRE. The install method is called to instantiate the applet. It is similar to the main method in standard Java applications. By default, this method always returns true, which means that the applet is ready to run. When the selected applet receives a command, it is passed for processing to the process method, which will be described later. To deactivate the applet, JCRE calls the deselect method. This method is empty by default. Using standard implementations of the listed methods (with the exception of the process method), they can be defined in the template as static content, and, if necessary, modified after generation to meet the requirements of a specific task. In the proposed approach, the entire logic of the process method is described by a hierarchical system of finite state machines, from which a code skeleton is generated that implements this logic. Automatic programming is supported by Switch technology [23]. Therefore, the process method consists of two nested switch statements, the outer one is used to iterate over states, and the inner one is used to iterate over commands. If the command received is valid for the current state, then the appropriate helper method is called; otherwise, an exception is raised that does not change the state of the applet. For helper methods, only stub methods are generated. According to the technology of automatic programming, transitions between states are marked with Boolean expressions formed from input actions. Provided that these expressions have no side effects, they can be preconditions for methods that are called upon entering a state. The structure of the transition graph can be specified using the constraint keyword and the \ old () expression. This specification is a disjunction of implications that describe the inbound and outbound transitions for each state. Moreover, it is possible to ensure that the applet is always in one of the predefined states (using a class invariant). The UniMod tool allows you to save the description of an automaton model in XML format. To generate the annotated code, a converter program developed during this work is used, which uses templates (also developed as part of this work) and Apache Velocity technology. 7. Methods for creating correct Java Card applications Based on the above, we present a description of the methodology for creating correct Java Card applications using the automaton approach:
Development of correct Java Card programs based on an automaton approach From the specification and terms of reference for the project, go to the UniMod description of the application. In this case, the host application is used as an event provider, and a smart card is used as a control object. 2. Verify the resulting model by the Model checking method using verifiers such as Spin or Bogor. 3. Export the UniMod-description of the application into XML-format using standard UniMod tools. 4. Submit the XML-description of the application and the templates created in the framework of this work to the input of the converter program developed by the authors for generating Java Card-code with JML-annotations. 5. Refine the manually generated code and JML-specification in the following directions: Implement the methods of input and output actions (a standard step in the framework of the automaton approach). Supplement JML annotations (mainly for input and output methods). 6. Verification can be carried out using the source code (7) or byte-code (8). 7. Depending on the problem being solved, submit the annotated code as input to one of the existing tools for checking the source code: jmlc runtime check. Static check ESC / Java2. Verification of KeY, LOOP, JACK. 8. Compile the code, translate the specification into byte-code and check it using the appropriate tools. 9. Manually handle error messages. 8. Conclusion Automata programming technology provides a methodology for developing robust embedded and reactive applications. In this paper, we propose its extension for creating Java Card applications, the additional guarantee of the correctness of which is the use of design by contract. In contrast to the already existing research on the verification of automata programs, this work proposes to combine various approaches to apply the verification of the source or byte code, and not only the Model checking technology. In this paper, it is proposed to start verification of the application with model verification using the Model checking technology. By isomorphically transferring the model to the source code level and supplementing the code and specification with a description of the behavior of input and output actions, it is possible to guarantee that the code corresponds to the already verified model and, in addition, the correctness of other methods, which could not be verified using only the Model checking technology. If necessary, a similar check can be carried out at the byte-code level. Therefore, verification can be carried out at all stages of application development and implementation. References 1. Chen, J. Java Card Technology for Smart Cards. Architecture and Programmer's Guide / J. Chen. M .: Technosphere, NASA LaRC Formal Methods Program: What is Formal Methods? 3. Shalyto, A. A. Algorithmization and programming for logical control systems and reactive systems / A. A. Shalyto // Automation and telemechanics / No 1. C
Modeling and analysis of information systems V.15, 3 (2008) 4. Poll, E. Specification of the JavaCard API in JML / E. Poll, J. van den Berg, B. Jacobs // Proc. Fourth Smart Card Research and Advanced Application Conference. P Coglio, A. An Approach to the Generation of High-Assurance Java Card Applets / A. Coglio // Proc. 2nd NSA Conf. on High Confidence Software and Systems (HCSS 02) P Hubbers, E. From finite state machines to provably correct Java Card applets / E. Hubbers, M. Oostdijk, E. Poll // Proc. 18th IFIP Inform. Security Conf P Hubbers, E. Generating JML specifications from UML state diagrams / E. Hubbers, M. Oostdijk // Proc. Forum on specification and Design Languages (FDL 03) P Gurov, V. S. UniMod - a tool for automaton programming / V. S. Gurov, M. A. Mazin, A. A. Shalyto // Scientific and technical bulletin. Fundamental and applied research of information systems and technologies. SPbSU ITMO Vol. 30. C (9. Development of verification technology for control programs with complex behavior, built on the basis of an automaton approach. Interim report on stage II Theoretical studies of tasks assigned to the research work. SPbSU ITMO, (10. Velder, S.E. Based on the Model checking method / S. E. Velder, A. A. Shalyto // Scientific and technical bulletin. Fundamental and applied research of information systems and technologies. methods of program verification / V.A.Nepomnyashchy, O.M. Ryakin M .: Radio and communication Kuzmin, E.V. About verification of automatic programs / E.V. Kuzmin, V.A. : Collection of articles for the 20th anniversary of the Faculty of ICT, YarSU named after P.G.Demidov. Yaroslavl, S (13. Korneev, G. A. Verification of automatic programs / G. A. Korneev, V. G. Parfenov, A. A. Shalyto // Abstracts of the International Scientific Conference dedicated to the memory of Professor A. M. Bogomolov Computer Science and technology Saratov: SSU C (14. Clarke, EM Formal methods: State of the Art and Future Directions / EM Clarke, JM Wing // ACM Computing Surveys. 1996, vol. 4. P Meyer, B. Object-oriented design of software systems / B. Meyer M .: Russian edition Leavens, GT Design by Contract with JML / GT Leavens, Y. Cheon // 17. Leavens, GT Preliminary design of JML: A behavioral interface specification language for Java. / GT Leavens , AL Baker, C. Ruby // Iowa State Univ., Dept. of Comput. Sci. Tech. Rep., Apr Burdy, L. An overview of JML tools and applications / L. Burdy et al. // Int. J. on Software Tools for Technology Transfer (STTT) Vol 7 (3). P Harel, D. On the Development of Reactive Systems / D. Harel, A. Pnueli // Logic and Models of Concurrent Systems. NATO Advanced Study Institute on Logic and Models for Verification and Specification of Concurrent Systems P Shalyto, A.A. Automated software design. Algorithmization and programming of logical control tasks / A. A. Shalyto // Izvestiya RAN. Theory and control systems С ( NATO Advanced Study Institute on Logic and Models for Verification and Specification of Concurrent Systems P Shalyto, A.A. Automated software design. Algorithmization and programming of logical control tasks / A. A. Shalyto // Izvestiya RAN. Theory and control systems С ( NATO Advanced Study Institute on Logic and Models for Verification and Specification of Concurrent Systems P Shalyto, A.A. Automated software design. Algorithmization and programming of logical control tasks / A. A. Shalyto // Izvestiya RAN. Theory and control systems С (
Development of correct Java Card programs based on the automaton approach Shopyrin, D.G.Synchronous programming / D.G.Shopyrin, A.A. Shalyto // Control information systems C (22. Shalyto, A.A. A. Shalyto // International Scientific and Technical Multiconference Problems of Information Technologies and Mechatronics. Materials of the International Scientific and Technical Conference Multiprocessor Computing and Control Systems. approach to the creation of software for reactive systems / A. A. Shalyto, N. I. Tukkel // Programming C (Automata-based approach for correct Java Card-program Klebanov AA, Shalyto AA The paper gives an overview of the research project which considers the generation of the dependable * Java Card * code.According to the automata-based programming technology, the code is generated from a high-level application behavior description which is based on finite state machines. An extra benefit from the use of such an approach is the possibility of the formal application specification generation. The conformance of the source or byte code against its specification could be checked by different static checking and verification tools.
Modeling and analysis of information systems V.15, 3 (2008) issued maps can be quite laborious and economically unprofitable. And finally, the limited resources and less functionality of the Java Card compared to Java technology ensures that programs do not have too complex behavior and a large number of control states [3]. Java Card applications can become a good training ground for various formal methods, on the one hand, the programs in this case are quite simple, and on the other hand, they are of specific practical interest, and not artificially created toy code. Thus, the task of applying formal methods for designing and verifying Java Card applications seems to be relevant and realizable. The purpose of this work is to expand the technology of automata programming to create correct Java Card programs. At the same time, it is necessary to solve a number of problems related to the implementation of the possibility of generating the skeleton of the source code of Java Card applications and their subsequent verification at the level of the source and byte codes. 2. Analysis of existing works It follows from the above that the analysis of existing works can be carried out in two directions, one of which is the generation of Java Card-code from high-level specifications, and the second is the verification of automatic programs. Generation of Java Card-code from high-level specifications There are two research projects, aimed at generating Java Card code from high-level specifications. The first of them [5] is based on the domain-specific language SmartSlang, which allows you to describe programs using high-level constructs typical of smart cards. However, it does not use an automaton approach, and therefore the project has little to do with the real work. The second project is considered in works [6, 7]. In these studies, the code is generated based on the state machine describing the applet. In [6], a verifier is used as an editor for finite state machines, and in [7], UML is used to describe automata. This work has several advantages over these studies. First, the technology of automata programming is used, which assumes the description of behavior by a hierarchical system of automata, and not just one automaton, as in [6, 7]. In [6], the question of modeling the host application itself and its interaction with a smartcard remains open. Allocating the host application as a separate event provider within the automaton approach sufficiently solves this issue. The notation used in automata programming technology hides the low-level features of the Java Card language, which facilitates the process of developing programs and increases their reliability. Indeed, the programmer is offered to operate not with byte arrays, but with short identifiers, for which a text description is always available. Second, the proposed approach generates a more complete specification. In particular, under certain restrictions, it is possible to generate preconditions for methods that are called upon entering a state. In [6], this question is referred to as open. Finally, a number of plugins have been developed for the UniMod tool [8], allowing verification of the automaton model [9]. Note that in [6] the verifier is used exclusively as a graphical editor for creating automata, and its use for its intended purpose is mentioned only in the section describing further studies. However, in a later work [7], model verification is not mentioned at all. Moreover, the issue of code generation is considered to be of secondary importance, and extracting an automaton model from the source code is considered an attractive task, which is opposite to the goal of this work. The most typical example of dynamic verification is testing. The essence of this method is to test the functionality of the program using some examples. Despite the widespread prevalence of this approach, it has a significant drawback of dependence on a specific scenario. It is well known (E. Dijkstra) that testing cannot prove the absence of errors in a program.
Development of Correct Java Card Programs Based on the Automata Approach 49 In this paper, the issue of application verification is considered as a matter of static verification, which includes Model checking technologies [10] and theorem proving [11]. When using the automaton approach, the Model checking technology plays a key role [10, 12, 13]. It allows you to automatically check whether a given requirement, expressed in the language of temporal logic, is fulfilled on the behavior model of a system with a finite number of states. Roughly speaking, the check is carried out using a search over the entire set of states, and the finiteness of the model ensures that the search will eventually complete. It is obvious that for general programs the use of this technology is very problematic. The model for verification has to be built heuristically. This raises the question of how adequate the resulting model is to the original program. However, Model checking is ideal for verifying automata programs. Indeed, this technology presupposes the formal construction of a model according to the program, which is a special kind of finite state machine. Therefore, the process of constructing a model from an automaton program can be automated, and, as a consequence, errors caused by the discrepancy between the model and the program will disappear. The writing of formal requirements for automaton programs is traditionally also simplified in comparison with constructed ones, since for this class of programs the semantic gap between the requirements for the program and the requirements for the model is practically eliminated in the course of constructing the automata. If an error occurs, a counterexample is issued; its translation into an automaton program can also be performed automatically. The disadvantage of Model checking technology as applied to automatic programming is that it covers only the logical part of the program. For the present work, another technology of verification, the method of proving theorems, is also important. Within the framework of this technology, both the system itself and the requirements for it are expressed using formulas of mathematical logic. Logic is defined by a set of axioms and inference rules, and the verification process consists in proving certain requirements. Unlike Model checking technology, theorem proving can be performed in the case of an infinite-dimensional state space. The disadvantage of this technology is the presence of non-existent error messages, often indicating a problem in the proof system, and not in the program itself. Model checking technology does not have this disadvantage. It is logical to raise the question of the possibility of combining these two technologies in such a way as to compensate for the shortcomings of each of them. Possible solutions are presented in a number of works. In work [14], devoted to the current state and prospects of formal methods, there is a remark that for the description and analysis of a complex system, most likely, it will not be enough to use only one formal method. Therefore, it becomes important to combine them. The main focus in this area is considered to be a combination of model checking and theorem proving technologies. Two approaches are proposed, firstly, to use Model checking as a decision-making tool for proving theorems, and secondly, using theorem proofs to obtain models in the form of finite automata and apply model checking to them. This work uses a different approach, which will be described in detail below. Its essence is that at different stages of the development and implementation of the application, it is proposed to apply various verification methods that are relevant for the current stage. In this case, it is possible to combine model verification with verification of its implementation, including verification of the byte code. Note that in [12] it is also stated that verification by the theorem-proving method is applicable to automatic programs. At the same time, however, it is argued that this approach is very laborious and useless for testing the logic of the program, and can only be used to test the input and output actions. In this work, an attempt is made to refute the first part of the statement (the second part is fully confirmed), firstly, a method for checking the program logic is described, and secondly, provides an overview of the tools (already existing and created within the framework of this work) that implement this check with a high degree of automation. 3. Methods and technologies used Before presenting the main part of the work, let us describe some of the methods and technologies on which it is based. The contract design methodology [15, 16] is used to develop reliable software. It proposes to consider the constituent parts of programs as the implementation of some formal specification, and not just as executable code. The main idea of this methodology is that the class and its clients enter into a contract with each other. The client must ensure that certain conditions are met before calling the class. For this, the class undertakes to fulfill implementing this check with a high degree of automation. 3. Methods and technologies used Before presenting the main part of the work, let us describe some of the methods and technologies on which it is based. The contract design methodology [15, 16] is used to develop reliable software. It proposes to consider the constituent parts of programs as the implementation of some formal specification, and not just as executable code. The main idea of this methodology is that the class and its clients enter into a contract with each other. The client must ensure that certain conditions are met before calling the class. For this, the class undertakes to fulfill implementing this check with a high degree of automation. 3. Methods and technologies used Before presenting the main part of the work, let us describe some of the methods and technologies on which it is based. The contract design methodology [15, 16] is used to develop reliable software. It proposes to consider the constituent parts of programs as the implementation of some formal specification, and not just as executable code. The main idea of this methodology is that the class and its clients enter into a contract with each other. The client must ensure that certain conditions are met before calling the class. For this, the class undertakes to fulfill The contract design methodology [15, 16] is used to develop reliable software. It proposes to consider the constituent parts of programs as the implementation of some formal specification, and not just as executable code. The main idea of this methodology is that the class and its clients enter into a contract with each other. The client must ensure that certain conditions are met before calling the class. For this, the class undertakes to fulfill The contract design methodology [15, 16] is used to develop reliable software. It proposes to consider the constituent parts of programs as the implementation of some formal specification, and not just as executable code. The main idea of this methodology is that the class and its clients enter into a contract with each other. The client must ensure that certain conditions are met before calling the class. For this, the class undertakes to fulfill The client must ensure that certain conditions are met before calling the class. For this, the class undertakes to fulfill The client must ensure that certain conditions are met before calling the class. For this, the class undertakes to fulfill
Modeling and analysis of information systems V.15, 3 (2008) other conditions after the completion of their work. The main advantage of the described methodology is the enforceability of contracts, the compiler translates them along with the source code. Therefore, any breach of contract during program execution can be detected immediately. Java Modeling Language (JML) [17] is a language for specifying Java modules (interfaces and classes) that describes both behavior and signature. JML is based on design-by-contract ideas and model-based specifications. The key elements of any specification are requires, ensures, and invariant. In the JML language there is an expression \ old (e) borrowed from Eiffel (a programming language developed to support design technology by contract [15]), which is equivalent to the value of expression E at the time of entering the body of the method. Changes to the value of a variable can be constrained using the constraint keyword, \ old () expression, and logical constructs such as a ==> b (implication) or a <==> b (equivalence). BOMs are written between or after. Thus, the standard Java compiler treats them as comments and simply ignores them. They are processed by specially developed means. To support JML, a large number of tools have been developed with different functionality [18]. The simplest way to check for code compliance with a specification is a runtime check, the JML compiler (jmlc) runs the annotated Java code and dynamically checks for type conformance and specification violations. Static verification (ESC / Java2) and formal verification (KeY, Loop, JACK) do not require launching the application and are able to solve much more complex problems, but with the help of the user and at the cost of some assumptions. Despite the fact that JML can be used to annotate arbitrary Java applications, at the moment the Java Card is considered the main area of its application [18]. 4. Statement of the problem and the scheme of the proposed solution Solving the problem of creating correct Java Card programs within the framework of using the automaton approach requires solving a number of subtasks: 1. Expand the existing technologies for generating code to obtain the possibility of creating a skeleton of Java Card applications from their automaton description. 2. Develop a method that allows you to generate a formal annotation to the code, covering the largest number of properties of the original automaton model. 3. Investigate existing tools for working with the JML language in order to identify suitable for solving diverse problems associated with the verification of annotated code. The general scheme of the proposed approach is shown in Fig. 1. It is proposed to solve the problem in several stages. On the first of them, a skeleton of the source code is generated from the automaton model, which describes the application logic with stubs for methods that implement input and output actions (solution of subproblem 1). In addition, a formal specification of the application in the JML language is generated (solution of subproblem 2). Then the input and output methods are manually implemented and, possibly, the application specification (JML annotation) is supplemented. Finally, using special tools, the compliance of the source code or byte code with the specification is checked (solution of subproblem 3). In this case, warnings about possible errors are issued to the user. 5. Automated approach for creating and verifying applications for smart cards In [19], it is proposed to divide systems into transforming and reactive systems. The transforming system processes the input information and issues a response based on it. The reactive system must constantly react to incoming influences. At the same time, it does not calculate any specific function, but maintains interaction with the environment. The reactive system stores its current internal state, and its response to the environment and state change are completely dependent on the input action and the current state. In this work, we use the automata programming proposed in [3, 20]. It is a kind of synchronous programming [21],
Development of Correct Java Card Programs Based on the Automaton Approach 51 Fig. 1. Scheme of the proposed approach According to the automaton programming paradigm [22], the program is considered as a system of automated control objects. At the same time, the program contains event providers, a control system consisting of interacting state machines, and control objects. Consider the features of the Java Card platform as a reactive system [19]. Interaction with a smartcard is carried out using card readers [1]. This device supplies power to the card and creates a communication channel between the card and the computer or terminal on which the host application is installed. The communication channel is half-duplex and uses the master-slave model. The smart card is always the slave and the host application is always the master. It means, that the smart card is always waiting for a command from the host application. The sequence of commands comes from the host application through the card reader in the Java Card Runtime Environment (JCRE). The commands are then passed to the selected applet. The applet processes the command and sends a response in the opposite direction. Thus, the interaction between the host application and the smart card can be interpreted as event-driven. Since the event providers of the host application and the smart card control object can be isolated, automatic programming can be effectively used to create robust Java Card programs (Figure 2). Rice. 2. Interpretation of automatic programming for the Java Card platform Application of the automatic approach does not free the programmer from writing code, since only that part of the functionality is generated that implements the logic of the system.
Modeling and analysis of information systems V.15, 3 (2008) manual creation of a code that implements input and output actions. The problem lies in the lack of means for checking the compliance of the code with its model and checking the methods that implement the input and output actions. The suggested way out of this situation is the use of contracts. Contracts also describe how different parts of a program interact, but they do so at a lower level of abstraction. If, along with the generation of the source code, a specification isomorphic to the model is generated, then, despite the lowering of the level of abstraction, the possibility of verification will remain. Therefore, the use of JML allows us to bridge the gap between the model and the specific implementation. Thus, it is possible to avoid the situation when the limited model causes unexpected errors in the program, or vice versa, errors in a poorly constructed model will signal non-existent errors in the program. In the case of verification of applications using JML, there is no need to build a formal model, the annotated source code itself is fed to the input of the verifier. As noted above, Model checking technology is limited only to checking the application logic, which is its main drawback. The generated code annotations allow you to accomplish similar tasks. However, if you add them manually, you can check a much larger amount of program properties, such as, for example, the behavior of methods that implement input and output actions, their interconnection, errors common in programming, such as an array index out of range, access to a nonexistent place in memory and much more. 6. Code and Specification Generation (Practical Implementation) All Java Card applets have a standard structure - they must override the methods of the base Applet class. To clarify the code generation process, we briefly describe [1] each of these methods in the order in which they are called by the JCRE. The install method is called to instantiate the applet. It is similar to the main method in standard Java applications. By default, this method always returns true, which means that the applet is ready to run. When the selected applet receives a command, it is passed for processing to the process method, which will be described later. To deactivate the applet, JCRE calls the deselect method. This method is empty by default. Using standard implementations of the listed methods (with the exception of the process method), they can be defined in the template as static content, and, if necessary, modified after generation to meet the requirements of a specific task. In the proposed approach, the entire logic of the process method is described by a hierarchical system of finite state machines, from which a code skeleton is generated that implements this logic. Automatic programming is supported by Switch technology [23]. Therefore, the process method consists of two nested switch statements, the outer one is used to iterate over states, and the inner one is used to iterate over commands. If the command received is valid for the current state, then the appropriate helper method is called; otherwise, an exception is raised that does not change the state of the applet. For helper methods, only stub methods are generated. According to the technology of automatic programming, transitions between states are marked with Boolean expressions formed from input actions. Provided that these expressions have no side effects, they can be preconditions for methods that are called upon entering a state. The structure of the transition graph can be specified using the constraint keyword and the \ old () expression. This specification is a disjunction of implications that describe the inbound and outbound transitions for each state. Moreover, it is possible to ensure that the applet is always in one of the predefined states (using a class invariant). The UniMod tool allows you to save the description of an automaton model in XML format. To generate the annotated code, a converter program developed during this work is used, which uses templates (also developed as part of this work) and Apache Velocity technology. 7. Methods for creating correct Java Card applications Based on the above, we present a description of the methodology for creating correct Java Card applications using the automaton approach:
Development of correct Java Card programs based on an automaton approach From the specification and terms of reference for the project, go to the UniMod description of the application. In this case, the host application is used as an event provider, and a smart card is used as a control object. 2. Verify the resulting model by the Model checking method using verifiers such as Spin or Bogor. 3. Export the UniMod-description of the application into XML-format using standard UniMod tools. 4. Submit the XML-description of the application and the templates created in the framework of this work to the input of the converter program developed by the authors for generating Java Card-code with JML-annotations. 5. Refine the manually generated code and JML-specification in the following directions: Implement the methods of input and output actions (a standard step in the framework of the automaton approach). Supplement JML annotations (mainly for input and output methods). 6. Verification can be carried out using the source code (7) or byte-code (8). 7. Depending on the problem being solved, submit the annotated code as input to one of the existing tools for checking the source code: jmlc runtime check. Static check ESC / Java2. Verification of KeY, LOOP, JACK. 8. Compile the code, translate the specification into byte-code and check it using the appropriate tools. 9. Manually handle error messages. 8. Conclusion Automata programming technology provides a methodology for developing robust embedded and reactive applications. In this paper, we propose its extension for creating Java Card applications, the additional guarantee of the correctness of which is the use of design by contract. In contrast to the already existing research on the verification of automata programs, this work proposes to combine various approaches to apply the verification of the source or byte code, and not only the Model checking technology. In this paper, it is proposed to start verification of the application with model verification using the Model checking technology. By isomorphically transferring the model to the source code level and supplementing the code and specification with a description of the behavior of input and output actions, it is possible to guarantee that the code corresponds to the already verified model and, in addition, the correctness of other methods, which could not be verified using only the Model checking technology. If necessary, a similar check can be carried out at the byte-code level. Therefore, verification can be carried out at all stages of application development and implementation. References 1. Chen, J. Java Card Technology for Smart Cards. Architecture and Programmer's Guide / J. Chen. M .: Technosphere, NASA LaRC Formal Methods Program: What is Formal Methods? 3. Shalyto, A. A. Algorithmization and programming for logical control systems and reactive systems / A. A. Shalyto // Automation and telemechanics / No 1. C
Modeling and analysis of information systems V.15, 3 (2008) 4. Poll, E. Specification of the JavaCard API in JML / E. Poll, J. van den Berg, B. Jacobs // Proc. Fourth Smart Card Research and Advanced Application Conference. P Coglio, A. An Approach to the Generation of High-Assurance Java Card Applets / A. Coglio // Proc. 2nd NSA Conf. on High Confidence Software and Systems (HCSS 02) P Hubbers, E. From finite state machines to provably correct Java Card applets / E. Hubbers, M. Oostdijk, E. Poll // Proc. 18th IFIP Inform. Security Conf P Hubbers, E. Generating JML specifications from UML state diagrams / E. Hubbers, M. Oostdijk // Proc. Forum on specification and Design Languages (FDL 03) P Gurov, V. S. UniMod - a tool for automaton programming / V. S. Gurov, M. A. Mazin, A. A. Shalyto // Scientific and technical bulletin. Fundamental and applied research of information systems and technologies. SPbSU ITMO Vol. 30. C (9. Development of verification technology for control programs with complex behavior, built on the basis of an automaton approach. Interim report on stage II Theoretical studies of tasks assigned to the research work. SPbSU ITMO, (10. Velder, S.E. Based on the Model checking method / S. E. Velder, A. A. Shalyto // Scientific and technical bulletin. Fundamental and applied research of information systems and technologies. methods of program verification / V.A.Nepomnyashchy, O.M. Ryakin M .: Radio and communication Kuzmin, E.V. About verification of automatic programs / E.V. Kuzmin, V.A. : Collection of articles for the 20th anniversary of the Faculty of ICT, YarSU named after P.G.Demidov. Yaroslavl, S (13. Korneev, G. A. Verification of automatic programs / G. A. Korneev, V. G. Parfenov, A. A. Shalyto // Abstracts of the International Scientific Conference dedicated to the memory of Professor A. M. Bogomolov Computer Science and technology Saratov: SSU C (14. Clarke, EM Formal methods: State of the Art and Future Directions / EM Clarke, JM Wing // ACM Computing Surveys. 1996, vol. 4. P Meyer, B. Object-oriented design of software systems / B. Meyer M .: Russian edition Leavens, GT Design by Contract with JML / GT Leavens, Y. Cheon // 17. Leavens, GT Preliminary design of JML: A behavioral interface specification language for Java. / GT Leavens , AL Baker, C. Ruby // Iowa State Univ., Dept. of Comput. Sci. Tech. Rep., Apr Burdy, L. An overview of JML tools and applications / L. Burdy et al. // Int. J. on Software Tools for Technology Transfer (STTT) Vol 7 (3). P Harel, D. On the Development of Reactive Systems / D. Harel, A. Pnueli // Logic and Models of Concurrent Systems. NATO Advanced Study Institute on Logic and Models for Verification and Specification of Concurrent Systems P Shalyto, A.A. Automated software design. Algorithmization and programming of logical control tasks / A. A. Shalyto // Izvestiya RAN. Theory and control systems С ( NATO Advanced Study Institute on Logic and Models for Verification and Specification of Concurrent Systems P Shalyto, A.A. Automated software design. Algorithmization and programming of logical control tasks / A. A. Shalyto // Izvestiya RAN. Theory and control systems С ( NATO Advanced Study Institute on Logic and Models for Verification and Specification of Concurrent Systems P Shalyto, A.A. Automated software design. Algorithmization and programming of logical control tasks / A. A. Shalyto // Izvestiya RAN. Theory and control systems С (
Development of correct Java Card programs based on the automaton approach Shopyrin, D.G.Synchronous programming / D.G.Shopyrin, A.A. Shalyto // Control information systems C (22. Shalyto, A.A. A. Shalyto // International Scientific and Technical Multiconference Problems of Information Technologies and Mechatronics. Materials of the International Scientific and Technical Conference Multiprocessor Computing and Control Systems. approach to the creation of software for reactive systems / A. A. Shalyto, N. I. Tukkel // Programming C (Automata-based approach for correct Java Card-program Klebanov AA, Shalyto AA The paper gives an overview of the research project which considers the generation of the dependable * Java Card * code.According to the automata-based programming technology, the code is generated from a high-level application behavior description which is based on finite state machines. An extra benefit from the use of such an approach is the possibility of the formal application specification generation. The conformance of the source or byte code against its specification could be checked by different static checking and verification tools.
