Home

le pdf - JFLA

1. automobile ou encore la m decine Il est donc indispensable d accompagner son d veloppement avec des m thodes renforc es de v rification du code ex cut Depuis quelques ann es le langage d annotations JML 21 enrichit dans ce but le langage de programmation objet Java Il permet d accro tre les possibilit s de v rification de la s ret du code source ou du bytecode g n r par le compilateur Java Cependant exprimer directement les conditions de s ret d un programme Java sous forme d annotations JML est fastidieux car les constructions de ce langage sont trop l mentaires Dans cet article nous expliquons comment g n rer ces annotations JML partir de propri t s de s curit de haut niveau de mani re automatique C est dans le logiciel pour carte puce que cette d marche a trouv ses premi res applications Pour en rendre compte nous en illustrons tous les aspects de l expression de propri t s jusqu la production d annotations avec l exemple de la classe APDU Application Protocol Data Unit de PAPI Java Card L article s organise comme suit La partie 2 pr sente l exemple de la classe APDU et le fragment du langage JML utilis pour traduire les propri t s en annotations La partie 3 d finit et compare deux formalismes compl mentaires pour l expression de propri t s de s curit Puis la partie 4 d crit la conception de l outil JAG Java Annotation Generator qui implan
2. curit des logiciels critiques Cependant pour tre adopt es par la communaut de d veloppement la plus large possible il est essentiel que ces m thodes soient appliqu es aux langages les plus populaires Ceci a t bien compris par les auteurs du langage d annotations JML dont la syntaxe est tr s proche du langage Java Ces annotations permettent d ex cuter de nombreux outils de v rification statique ou dynamique du code annot Ind pendamment les sch mas de propri t s temporelles de Dwyer et al ont t concus pour rendre l expression de propri t s temporelles plus accessible aux programmeurs Ces efforts ont t unifi s gr ce au langage JTPL qui a t choisi pour cette raison comme premier format d entr e de l outil de g n ration d annotations JML pr sent ici Depuis nous avons compl t cet outil avec un formalisme d automates galement pr sent ici Ainsi notre outil de g n ration automatique d annotations JML s int gre naturellement dans une cha ne logicielle qui permet au programmeur Java de v rifier des propi t s temporelles en 88 Un programme annot en vaut deux assimilant un minimun de connaissances suppl mentaires La particularit et l un des atouts de ce travail est de g n rer des annotations JML standard sur lesquelles l ensemble des outils JML peuvent tre appliqu s Afin de rendre cette chaine logicielle plus op rationnelle nous travaillons actuelle
3. nous proposons la possibilit d exprimer des propri t s temporelles l aide d automates d tats finis Ce format d automates est inspir d une proposition d un partenaire industriel qui utilisait des diagrammes d tats UML pour exprimer le comportement de ses applications Java Card Les automates taient alors transform s manuellement en annotations JML Cette traduction manuelle avaient comme d fauts d tre d une part fastidieuse et d autre part source potentielle d erreurs Nous avons donc con u une traduction automatique de ces automates en annotations JML Les automates en question sont des automates d tats finis dont les transitions sont tiquet es par des v nements JTPL m called m terminates Nous illustrons cette approche avec la classe APDU de la Java Card qui supporte quatre modes de transmission de message NO DATA pas de donn es en entr e pas de donn es en r ponse IN donn es en entr e pas de donn es en r ponse OUT pas de donn es en entr e donn es en r ponse IN OUT donn es en entr e et en r ponse Chacun de ces modes correspond une s quence particuli re d invocations de m thodes de la classe APDU Ces s quences sont plus faciles d crire par un automate comme celui de la figure 3 que par un ensemble de formules JTPL receiveBytes called etIncomingAndReceive calle sendBytes called setOutgoingLength called s
4. Canada August 2006 Springer F Bouquet B Legeard and N Vacelet BZP Un format f d rateur pour l valuation de sp cifications formelles In JFPLC 03 Journ es Francophones de Programmation en Logiques et Contraintes pages 203 216 Amiens France June 2003 Hermes TSI L Burdy Y Cheon D Cok M Ernst J Kiniry G T Leavens K R M Leino and E Poll An overview of JML tools and applications In Th Arts and W Fokkink editors Eighth International Workshop on Formal Methods for Industrial Critical Systems FMICS 03 volume 80 of ENTCS pages 73 89 Elsevier 2003 7 8 89 Giorgetti amp Groslambert 9 L Burdy and A Requet Jack Java applet correctness kit In Gemplus Developers Conference GDC2002 2002 10 L Burdy A Requet and J L Lanet Java applet correctness A developer oriented approach In FME 2003 volume 2805 of LNCS pages 422 439 Springer 2003 11 Y Cheon and G T Leavens A runtime assertion checker for the Java Modeling Language JML Technical Report 02 05 Department of Computer Science Iowa State University March 2002 In SERP 2002 pp 322 328 12 M B Dwyer G S Avrunin and J C Corbett Patterns in property specifications for finite state verification In International Conf on Software Engineering pages 411 420 IEEE Computer Society Press ACM Press 1999 13 E A Emerson Temporal and modal logic In J van Leeuwen editor Handbook of Th
5. algorithmique ou la preuve de code Java annot en JML peuvent setOutgoingNoChaining remplace setOutgoing quand le terminal de la carte ne supporte pas un mode particulier appel block chaining Ces consid rations techniques n entrent pas en jeu dans la compr hension de l exemple 81 Giorgetti amp Groslambert tre utilis s en aval de JAG 4 1 Principe de fonctionnement La structure de l outil est illustr e par la figure 6 Le fichier Java JML d entr e est analys syntaxiquement par l outil JMLTools 11 Les propri t s temporelles JTPL sont analys es avec un analyseur syntaxique produit avec le m me g n rateur ANTLR que celui de JMLTools afin de faciliter une int gration ult rieure La version actuelle 0 2 de JAG permet de d crire les automates de la partie 3 2 dans le langage Promela 20 Un extrait de la description Promela de l automate de l APDU de la figure 3 est donn dans la figure 4 La prochaine version de JAG permettra l utilisateur de dessiner son automate dans un environnement graphique de conception de diagrammes d tats UML Elle comportera un traducteur vers ce format Promela L outil JAG g n re automatiquement les variables ghost qui encodent l automate Un extrait du fichier de sortie obtenu pour la classe APDU est donn dans la figure 5 Fichier Arbre de Source Analyse syntaxe Generation Creation JAVA JML Syntax
6. Java Modeling Language In Formal Underpinnings of Java Workshop at OOPSLA 798 October 1998 22 G Nelson Techniques for Program Verification PhD thesis Stanford University 1980 23 A Pnueli The temporal logic of program In 18th Ann IEEE Symp on foundations of computer science pages 46 57 1977 24 S Ranise and D Deharbe Light weight theorem proving for debugging and verifying units of code Proc of the International Conference on Software Engineering and Formal Methods SEFM03 IEEE Computer Society Press Camberra Australia September 2003 25 The Coq Development Team The Coq Proof Assistant Reference Manual Version V7 1 October 2001 http coq inria fr 26 K Trentelman and M Huisman Extending JML Specifications with Temporal Logic In H Kirchner and C Ringeissen editors Algebraic Methodology And Software Technology AMAST 02 number 2422 in LNCS pages 334 348 Springer 2002 27 Pierre Wolper Temporal logic can be more expressive In FOCS pages 340 348 IEEE 1981 90
7. ace est la suivante always P est vraie sur une ex cution o si P est satisfaite sur chaque tat de o eventually P est vraie sur une ex cution o si P est satisfaite sur au moins l un des tats de Oo la s mantique de la conjonction et de la disjonction est standard 78 Un programme annot en vaut deux always P GP after E always P G E GP before E always P FE PUE always P until PUE always P unless PUE V GP after E1 always P until 2 G E1 PUE2 after E always P unless E2 G E1 PUE2 V GP eventually P FP after E eventually P G E FP before E eventually P FE PUE eventually P until FE PUE eventually P unless FE PUE V FE AFP after Fy eventually P until E2 G E1 FE2 A PUE after Fy eventually P unless E2 G E1 FE2 PUE V FE2 A FP Fic 2 Traduction de quelques formules JTPL en LTL Il est bien souvent utile de r duire la port e d une propri t de trace une sous s quence de Vex cution Ceci est rendu possible en JTPL par la notion d v nement Un v nement peut tre m called qui signifie que la m thode m vient d tre appel e i e a t appel e dans l tat pr c dant imm diatement l tat courant m normal qui signifie que la m thode m a termin normalement c est dire sans lever d exception m exceptional qui signifie que la m thode m a termin en levant une
8. actioncalled_2 gt TrDepth false TrDepth true invariant bufferPosition lt buffer length gTLcommitTransactionterminates_1i amp amp TrDepth true gTLabortTransactionterminates_1 Qx gt bufferPosition 0 public void beginTransaction set gTLbeginTransactioncalled_2 true invariant buffer length bufferPosition gt 0 set gTLcommitTransactioncalled_1 false set gTLabortTransactioncalled_1 false constraint bien old gTLbeginTransactioncalled_2 Fic 10 Extrait d un fichier de sortie de l outil JAG sont g n r es automatiquement en m moire 4 G n ration du fichier de sortie En cliquant sur le bouton Choose Output File choisir un fichier de sortie une bo te de dialogue s ouvre afin de choisir le nom et l emplacement du fichier de sortie JAG cr e alors le fichier de sortie en parcourant le fichier d entr e et en ajoutant les annotations g n r es partir des propri t s temporelles voir figure 10 Le r sultat de la g n ration est enregistr dans le fichier s lectionn et il est affich dans le cadre de droite 3 La tra abilit est visualis e ici car les annotations g n r es sont affich es de la m me couleur que la propri t temporelle dont elles sont issues Dans la figure 10 le premier invariant assure la satisfaction de la propri t de s ret i Le second assure que le variant de la pr
9. ariant getBuffer length gt 37 ghost int bufferPosition 0 void sendBytes short bOff short len byte pure getBuffer normal_behavior short setIncomingAndReceive requires bufferPosition 0 ensures bufferPosition bOff 1 short setQutgoing bufferPosition getBuffer length void setOutgoingAndSend short bOff short len short receiveBytes short bOff ites PE le getBuffer length set bufferPosition void setOutgoingLength short len Off gt le le bOff 1 short setQutgoingNoChaining Fic 1 Extrait de la classe APDU annot e en JML Thttp java sun com products javacard htmldoc javacard framework APDU html 77 Giorgetti amp Groslambert 2 1 Propri t s v rifier Sur la classe APDU on souhaite v rifier deux propri t s de bon fonctionnement exprim es informellement en anglais par Sun Microsystems dans la documentation HTML de la classe i un appel la m thode setIncomingAndReceive d clenche une exception si elle a d j t appel e auparavant avec succ s et ii la m thode setOutgoingLength ne peut pas tre appel e a moins que la m thode setOutgoing n ait t appel e avec succ s auparavant Ces propri t s de s curit peuvent tre cod es comme des restrictions sur les s quences d ex cution de m thodes Java Toutefois il n est pas ais de les tradui
10. asse Java que l on veut v rifier et ou de consulter la liste des obligations de preuves g n r es Le cadre B affiche des statistiques sur la g n ration d obligations de preuve pourcentage des obligations de preuve actuellement prouv es temps n cessaire la r alisation des preuves et des informations relatives l obligation de preuve que l on est en train de consulter le cadre affiche par exemple le but qui est prouver et les hypoth ses disponibles Enfin le cadre C affiche la classe Java s lectionn e en colorant les annotations JML et les portions de code Java correspondant l obligation de preuve s lectionn e Nous chargeons le fichier de sortie g n r par JAG dans l outil Jack et nous lan ons la g n ration des obligations de preuve en choisissant la sortie vers le prouveur automatique Simplify 22 Shttp www eclipse org 86 Un programme annot en vaut deux File Edit Navigate Search Project ecleTeX Menu Run JML Window Help Civ amp amp JMLProve JMLProve Q ES G Jack amp Java S Team Sync CVS R gt Gv oy case Ex 38 1 E case Viewer Lemma 85 Proved 83 97 Checked 0 0 53 Dw normal_behavior a requires trDepth true void commitTransaction 7 TransactionSystemBufferTL j7 set grLbeginTransactioncalled_0 false v commitTransaction set gTLcommitTransacti
11. e exhib e en g n rant automatiquement avec JML TT des tests orient s par la propri t temporelle 5 Nous la corrigeons donc en ajoutant la ligne de code bufferPosition 0 dans le corps de la m thode commitTransaction Pour la seconde obligation de preuve dont la preuve a chou en utilisant nouveau l interface de JAG nous trouvons qu elle concerne aussi la propri t temporelle i La propri t i peut ne pas tre satisfaite par un appel la m thode modify quand aucune transaction n est en cours apr s un commit ou un abort et avant un appel beginTransaction Cependant dans ce cas la pr condition de modify ne peut pas tre satisfaite c est a dire que modify ne peut pas tre appel e donc il n y a pas d erreur de programmation C est la propri t temporelle qui n est pas assez pr cise On la compl te en ajoutant la n gation de la pr condition de modify ce qui donne after commitTransaction terminates abortTransaction terminates before beginTransaction called always bufferPosition amp amp trDepth true amp amp bufferPosition lt buffer length Ainsi l ensemble des obligations de preuve est prouv de mani re automatique et les deux propri t s temporelles sont satisfaites par la classe Java 6 Conclusion et travaux futurs Nous sommes convaincus que les m thodes formelles de v rification du logiciel ont un r le essentiel jouer dans la s
12. eoretical Computer Science volume B Formal Models and Semantics chapter 14 pages 996 1072 Elsevier 1990 14 J C Filli tre Verification of Non Functional Programs using Interpretations in Type Theory Journal of Functional Programming 13 4 709 745 July 2003 15 J C Filli tre Why a multi language multi prover verification tool Research Report 1366 LRI Universit Paris Sud March 2003 16 Jean Christophe Filli tre and Claude March Multi prover verification of c programs In 6th International Conference on Formal Engineering Methods ICFEM 2004 number 3308 in LNCS pages 15 29 Seatle 2004 17 J Groslambert A JAG extension for verifying LTL properties on B event systems In B 2007 the 7th Int B Conference Tool Session volume 4355 of LNCS pages 262 265 Besancon France January 2007 Springer To appear 18 J Groslambert Verification of LTL on B event systems In B 2007 the 7th Int B Conference volume 4355 of LNCS pages 111 125 Besancon France January 2007 Springer To appear 19 J Groslambert J Julliand and O Kouchnarenko JML based verification of liveness properties on a class In SAVCBS 06 Specification and Verification of Component Based Systems pages 41 48 Portland Oregon USA November 2006 20 G J Holzmann The model checker SPIN In IEEE Trans on Software Engineering volume 23 5 pages 279 295 1997 21 G T Leavens A L Baker and C Ruby JML a
13. etOutgoingNoChaining called sendBytes called setOutgoingLength called setOutgoingAndSend called Fic 3 Automate de VAPDU Dans l tat initial 1 la m thode setIncomingAndReceive peut tre invoqu e pour entrer 80 Un programme annot en vaut deux never Ti_init public class APDU if sue setIncomingAndReceive called ghost int APDUstate 1 gt goto accept_S2 invariant APDUstate gt 1 setOutgoing called invariant APDUstate lt 7 gt goto accept_S3 aba setOutgoingNoChaining called gt goto accept_S5 requires APDUstate 1 setOutgoingAndSend called assignable APDUstate gt goto accept_S7 ensures APDUstate 2 fi Qx accept_S2 void setIncomingAndReceive if set APDUstate 2 receiveBytes called gt goto accept_S3 fi J Fic 4 Extrait du fichier de description F1G 5 Extrait de la sortie de JAG pour Promela VAPDU dans le mode IN ou le mode IN OUT On peut alors invoquer la m thode receiveBytes pour lire la donn e d entr e Ensuite la m thode setOutgoingAndSend resp setOutgoing et setOutgoingNoChaining peut tre invoqu e pour renvoyer une r ponse sans donn es pour les modes IN et NO DATA resp avec donn es pour les modes OUT et IN OUT Quand des donn es de r ponse doivent tre envoy es modes OUT et IN OUT la m thode setOutgoingLength est invoqu e pour donner la longueur de la r ponse Enfin la m thode sendBytes e
14. exception m terminates qui signifie que la m thode m a termin en levant ou non une exception Enfin une propri t JTPL est soit une propri t de trace soit l une des constructions suivantes o E est un ensemble d v nements C est une propri t JTPL et T est une propri t de trace after E C qui est satisfaite sur une ex cution o si chaque suffixe de o commen ant apr s une occurrence d un v nement de E satisfait la propri t C before E T qui est satisfaite sur une ex cution o si chaque pr fixe de o terminant par une occurrence d un v nement de E satisfait la propri t de trace T T until E qui est satisfaite sur une ex cution o si un v nement de E appara t in vitablement et si la propri t de trace T est satisfaite sur le segment de o pr c dant cet v nement de EF T unless FE qui est satisfaite sur une ex cution o si un v nement de F a lieu et si la propri t de trace T est satisfaite sur le segment de o pr c dant cet v nement de E ou si T est satisfaite sur toute l ex cution o et si aucun v nement de E n a lieu La logique JTPL est une logique lin aire incluse dans la LTL logique temporelle lin aire 13 Des exemples de traduction de formules JTPL en LTL sont donn s dans la figure 2 Dans cette figure E d signe en JTPL un ensemble d v nements tandis qu il d signe en LTL le pr dicat caract ristique des tats qui succ dent imm diate
15. ier n r es matiques TransactionSystem 92 I Atin Transaction man Electronic Purse 500 2 25 14 12 lignes de JML TAB 1 R sultats exp rimentaux De plus la sp cification JML du porte monnaie a t utilis e pour g n rer des tests avec loutil JML TT 6 Ces tests ont ensuite t ex cut s sur l application elle m me Enfin Voutil JAG a encore t utilis pour valider une impl mentation Java du porte monnaie lectronique 5 Les annotations ont dans ce cas t directement g n r es dans le code Java de l impl mentation et ont t v rifi es l ex cution des tests par le v rificateur d annotations JML la vol e JML RAC Runtime Assertion Checker des JMLTools 5 Exemple d utilisation Dans cette partie nous expliquons comment utiliser l outil JAG et comment le combiner avec le g n rateur d obligations de preuve Jack 10 qui confronte les annotations JML avec le code de la classe annot e Ce tutoriel est fond sur un exemple simple de syst me de transactions 5 1 Exemple illustratif Nous illustrons la d marche de v rification avec JAG et Jack sur l exemple pr sent dans la figure 8 Il s agit d une classe qui implante un syst me de transactions avec tampon buffer Dans cette classe une m thode beginTransaction d marre une nouvelle transaction et une m thode commitTransaction la valide Durant la transaction une m thode modify crit dans un tampon temp
16. inTrancachancallad 9 N M V TransactionSystemBufferTL v commitTransaction Goal 1 D modify byte Fic 12 Tra abilit des obligations de preuve de Jack Fic 13 Tra abilit des annotations de JAG 87 Giorgetti amp Groslambert 5 4 Tra abilit des annotations et diagnostic La tra abilit des annotations implant e dans JAG permet d aider l utilisateur en cas d chec de la preuve comme c est le cas ici Deux cas sont alors envisager Soit la propri t que l on veut prouver n est pas satisfaite ce qui indique la pr sence d une erreur dans le programme Soit la propri t est satisfaite mais la preuve est trop complexe pour tre r alis e de mani re automatique En particulier cela peut arriver lorsque le prouveur manque d hypoth ses pour tablir automatiquement le but de l obligation de preuve Gr ce la coloration de l interface de JAG illustr e par la figure 13 on trouve que cet invariant a t g n r partir de la propri t temporelle i qui signifiait qu apr s tout appel de la m thode commitTransaction le tampon buffer devait tre vide Dans le code source de la m thode commitTransaction qui est statut buffer set trDepth false nous constatons que la variable bufferPosition n est pas remise 0 L erreur venait donc d une mauvaise impl mentation du code source On peut noter que cette erreur aurait pu tr
17. ique abstraite d annotations du fichier Java JML JML de sortie Fichier Arbre de nf Contenant syntaxe A Primitives ne i Analyse abstraite Traitement Java JML les ia avec formules Syntaxique formules Interne done temporelles temporelles Fic 6 Sch ma g n ral de l outil Le processus de g n ration des annotations JML a d j t d crit dans des publications pr c dentes 2 26 19 L outil r duit tout d abord chaque formule temporelle v rifier en une ou plusieurs primitives interm diaires qui lui sont s mantiquement quivalentes La primitive Inv repr sente la partie s ret d une propri t temporelle la primitive Loop repr sente sa partie vivacit et la primitive Witness repr sente un tat particulier du syst me ou de l ex cution Ces primitives optimisent l tape suivante de g n ration d annotations JML quivalentes L utilisation de ces primitives permet ensuite de factoriser le travail de g n ration d annotations L utilisation de primitives pourra galement permettre d envisager des extensions futures l outil JAG Une adaptation aux syst mes d v nements B existe d j 17 18 et une extension au langage d annotations SPEC 1 est en cours de d veloppement 4 2 G n ration d annotations JML partir des primitives Chaque primitive Inv est traduite en un invariant JML ou en une postcondition de m thode Chaque primitive L
18. ir un variant under variant un entier naturel qui doit d cro tre strictement chaque appel de m thode pour garantir qu on finira par atteindre l tat voulu 51 n tait pas possible d illustrer ce tutoriel avec la classe APDU car son code source requis pour l utilisation de Jack n est pas diffus 84 public class TransactionSystem final int LENGTH 30 byte status new byte LENGTH byte buffer new byte LENGTH int bufferPosition 0 invariant buffer null invariant buffer length LENGTH invariant bufferPosition lt LENGTH amp amp bufferPosition gt 0 ghost boolean trDepth false requires trDepth false void beginTransaction Un programme annot en vaut deux requires trDepth true void abortTransaction bufferPosition 0 set trDepth false buffer new byte LENGTH set trDepth true requires trDepth true void commitTransaction status buffer set trDepth false requires trDepth true amp bufferPosition lt buffer length Qx void modify byte b buffer bufferPosition b bufferPositiont Fic 8 Exemple illustratif Un syst me de transactions amp SwingApplication Choose Input File TransactionSystem java Choose Property File pl tot property ies package jtpl java jrnlts public class TransactionS
19. it de l outil Jack illustr e dans la figure 12 Celle ci permet facilement de d terminer que la premi re obligation de preuve correspond l invariant g n r suivant invariant gTLcommitTransactionterminates_1 gTLabortTransactionterminates_1 gt bufferPosition 0 Ceci signifie que l outil ne parvient pas prouver que cet invariant est pr serv par l ex cution des m thodes commitTransaction et modify Pour poursuivre cette analyse on utilise la tracabilit de JAG comme d taill dans la partie suivante jm v yon Package A lcase Viewer Lemma 85 Proved 83 9 Choose Property File ransacationSystemBuff private invariant gTLcommitTransactioncalled_0 gTLabortTransactioncalled_1 ae See eons lcommitrransactiong es oy _ RbortTransaction called private invariant gTLbeginTransactionc always bufferPosition private invariant gTLbeginTransaction private invariant buffer length bufferP 0 junless private constraint old gTLbeginTransac ASU canen private constraint old gTLbeginTransac Choose Output File TransactionSystemBufferTLjava ATUT_LENGTH invariant bufferPosition STATUT_LENGTH invariant bufferPositio private invariant gTLcommitTransactioncalled_0 gTLabortTransactioncalled_1 bufferPosition private invariant ATI han
20. janvier 2007 s Journ es Francophones des Langages Applicatifs JFLA07 Un programme annot en vaut deux A Giorgetti amp J Groslambert LIFC FRE CNRS 2661 Universit de Franche Comt 16 route de Gray 25000 Besancon cedex France giorgetti groslambert lifc univ fcomte fr R sum La s curit du logiciel passe par les m thodes formelles mais comment faire passer les m thodes formelles dans le monde r el du d veloppement des logiciels critiques Cet article propose un m canisme et un outil d aide a la v rification de code par r duction automatique de propri t s de s curit en annotations formelles Ce dispositif s applique aux programmes Java annot s en JML Il est illustr ici par annotation automatique d une classe de l API Java Card Deux formalismes compl mentaires pour l expression de propri t s sont propos s L outil JAG qui implante leur r duction en annotations JML est d crit en d tail Le langage d annotations retenu JML tant standard cet outil s interface naturellement avec de nombreux outils existants pour la v rification par preuve test ou model checking de Java annot en JML Mots cl s logiciel s r Java Modeling Language propri t s temporelles annotations v rification 1 Introduction Le logiciel devient de plus en plus incontournable dans des domaines o la s curit est primordiale comme les transports les communications l a ronautique l
21. ment l un de ces v nements Les sch mas JTPL sont cependant strictement moins expressifs que les formules LTL sur les m mes propri t s d tats Par exemple la propri t d quit infiniment souvent P qui peut s crire GFP en LTL n est pas expressible en JTPL En revanche les sch mas JTPL sont plus simples comprendre et utiliser que les formules LTL ou CTL logique arborescente 13 tout en couvrant les besoins les plus courants 12 Par exemple les propri t s JTPL before E always P et after E1 always P unless EF s criraient respectivement FE PUE et G E PUE2 V GP en LTL 3 1 2 Exemples de propri t s temporelles En JTPL les deux propri t s de la partie 2 1 peuvent s exprimer comme suit 79 Giorgetti amp Groslambert i after setIncomingAndReceive normal always setIncomingAndReceive not enabled ii always setOutgoingLength not enabled unless setOutgoing normal La premi re formule signifie qu apr s after un appel r ussi la m thode set IncomingAnd Receive setIncomingAndReceive normal tout autre appel a cette m thode doit lever une exception always setIncomingAndReceive not enabled La seconde formule traduit que tout appel la m thode setOutgoingLength l ve une exception moins unless qu un appel la m thode setOutgoing n ait r ussi setOutgoing normal 3 2 V rification base d automates Outre le langage JTPL
22. ment i e lorsque l v nement setOutgoing normal appara t durant l ex cution Une postcondition est ajout e la m thode set IncomingAndReceive qui assure que lorsque dans le pass la m thode set IncomingAndReceive a d j t invoqu e avec succ s la variable gTLset IncomingAndReceive_normal a la valeur true la m thode ne pourra terminer normalement i e sa postcondition sera obligatoirement valu e faux De m me tant que la variable gTLsetOutgoing_normal n aura pas la valeur true i e la m thode setOutgoing n aura pas termin normalement la postcondition de setOutgoingLength ne pourra tre tablie 4 3 Tra abilit des annotations g n r es Une tra abilit des annotations JML g n r es a t implant e dans l outil JAG L interface graphique de JAG permet partir d une annotation g n r e de retrouver la primitive et la propri t temporelle d origine D obtenir des informations sur ce que v rifie chacune des annotations d croissance de variant observation d appel de m thode Cette caract ristique permet un diagnostic plus ais en cas d chec de la v rification d une annotation JML en particulier pour la recherche automatique de contre exemples Dans un travail pr liminaire 5 nous avons montr comment g n rer des cas de test conformes une propri t JTPL L ex cution de ces tests avec v rification la vol e des annotations JML permet soi
23. ment dans deux directions principales Tout d abord nous tendons la g n ration d annotations d autres formalismes d entr e en particulier la LTL 23 et aux diagrammes d tats UML 2 0 Parall lement nous pr parons une int gration plus forte de JAG avec les outils en aval en particulier avec les outils de g n ration d obligations de preuve JML2B Krakatoa et Jack En particulier une int gration plus forte avec Krakatoa consisterait g n rer directement un quivalent des annotations JML dans le format interm diaire de WHY 14 15 en ajoutant les variables et invariants n cessaires Une telle int gration permettrait de v rifier de mani re similaire les programmes Java JML mais galement les programmes C annot s avec Caduceus 16 La r alisation effective d une chaine logicielle int gr e de v rification et ou de validation des propri t s temporelles n cessiterait une importante coop ration entre trois formats f d rateurs Le format WHY pour la g n ration des obligations de preuve le format BZP 7 pour la validation par animation symbolique g n ration de tests et recherche de contre exemples et le format interne de repr sentation de propri t s temporelles et d annotations de l outil JAG L outil JAG et sa documentation sont disponibles en t l chargement l adresse http www lifc univ fcomte fr jag Remerciements Les auteurs tiennent remercier les relecteurs de la per
24. nvoie la donn e de r ponse Dans cet automate le mot vide marque une transition sans v nement Ceci signifie qu partir de l tat 1 les m thodes setIncomingAndReceive setOutgoing setOutgoingNoChaining et setOutgoingAndSend peuvent tre invoqu es Cette notation facilite encore l criture de tels automates L int r t des automates est double D un point de vue th orique il existe des propri t s exprimables par automate qui ne sont pas expressibles en LTL donc a fortiori en JTPL 27 Par exemple la propri t La m thode m est appel e dans chaque tat index par un nombre impair ne peut pas tre exprim e en LTL D un point de vue pratique certaines propri t s sont plus faciles exprimer sous forme d automate Par exemple l automate de la figure 3 inclut outre les propri t s JTPL i et ii de la partie 3 1 2 un grand nombre de propri t s similaires autorisant ou interdisant certains encha nements de m thodes 4 JAG un g n rateur d annotations JML Cette partie pr sente la version 0 2 de l outil JAG pour JML Annotation Generator qui permet partir d un fichier Java JML et d une propri t de s curit formalis e en JTPL ou par un automate de g n rer les annotations JML Java Modeling Language appropri es la v rification de cette propri t Le code JML produit tant standard tous les outils existants 8 pour la validation la v rification
25. oncalled_1 true v Q Case 1 statut buffer set trDepth false x Goal 2 7 modify byte v Case 1 normal_behavior requires trDepth true void abortTransaction set gTLbeginTransactioncalled_0 false set gTLabortTransactioncalled_2 true bufferPosition 0 Goal 3 set trDepth false gt Jack Metrics View Jack Proof View gt Check member invariant 53 o 8 this trDepth REFERENCES TransactionSystemBufferTLan_instance rad REFERENCES this gt TransactionSystemBufferTLan_instance instances this instances gt typeof TransactionSystemBufferTLan_instance lt Transac typeof this lt TransactionSystemBufferTL gt TransactionSystemBufferTLan_instance gTLcommitTransi forall REFERENCES TransactionSystemBufferTLan_instance v TransactionSystemBufferT Lan_instance gTLabortTransactio 4 gt lt gt Java B BDisplayed Coq PVS Simplify 3 TLFacto J PPAsser B Transac 8 BACKUPT B Transac E Transac D Transac 16 m F G 11 Interface principale de Jack L interface de Jack nous informe alors que 85 obligations de preuve ont t g n r es et que 83 d entre elles ont t v rifi es automatiquement Pour les deux obligations de preuve qui restent a prouver on utilise la tracabil
26. oop est traduite en un ensemble d invariants et de contraintes historiques qui impliquent la d croissance du variant et l absence de blocages Chaque primitive Witness est traduite par une variable ghost L outil produit en sortie un fichier dans lequel la classe originale est compl t e avec les annotations JML g n r es La figure 7 pr sente un extrait de la sp cification obtenue pour la Shttp www antlr org 4Le fichier complet est disponible depuis la page http lifc univ fcomte fr jag 82 Un programme annot en vaut deux ghost public boolean gTLsetIncomingAndReceive_normal false public short setOutgoing ghost public boolean it gTLsetQutgoing normal false set gTLsetOQutgoing normal true Q private normal_behavior Q private normal_behavior srs Psa ensures old gTLset IncomingAndReceive_normal ensures old gTLsetOutgoing_normal public short setIncomingAndReceive public void setQutgoingLength short len set gTLsetIncomingAndReceive_normal true Fic 7 Extrait d un fichier de sortie de l outil JAG v rification des propri t s i et ii sur la classe APDU On peut constater que des variables ghost sont ajout es pour observer les appels et terminaisons des m thodes impliqu es dans la formule temporelle Par exemple la valeur true est donn e la variable gTLsetOutgoing_normal lorsque la m thode setOutgoing termine normale
27. opri t de vivacit ii est bien un entier naturel Les deux contraintes historiques constraint assurent respectivement que ce variant diminue apr s chaque appel de m thode jusqu a la terminaison de la transaction et qu il n y a pas de blocage avant la terminaison de la transaction au moins une des pr conditions de m thode est vraie Cela est obtenu en g n rant la disjonction des pr conditions des m thodes Le lecteur pourra remarquer que dans le cas pr sent la derni re contrainte historique est trivialement satisfaite 5 3 V rification des annotations g n r es Pour v rifier que le code Java est bien conforme aux annotations g n r es on peut utiliser n importe lequel des outils de v rification pour JML Nous utilisons ici l outil Jack 10 qui est un g n rateur d obligations de preuve partir du code Java et des annotations JML Jack g n re un ensemble de formules logiques appel es obligations de preuve La satisfaction de ces obligations de preuve implique la correction du code Java vis vis des annotations JML La v rification de cette satisfaction des obligations de preuve est confi e des outils de preuve automatique ou interactive comme Simplify 22 Coq 25 ou haRVey 24 Jack est distribu sous la forme d un plug in de l environnement de d veloppement Eclipse Ce plug in ajoute un environnement sp cifique qui est pr sent dans la figure 11 Le cadre A permet de s lectionner la cl
28. oraire La transaction peut tre abandonn e par invocation d une m thode abortTransaction Les deux propri t s que l on souhaite v rifier sont les suivantes i Le buffer doit tre vid avant de commencer une nouvelle transaction et ii toute transaction commenc e doit fatalement se terminer En JTPL ces deux propri t s peuvent s exprimer comme suit i after commitTransaction terminates abortTransaction terminates before beginTransaction called always bufferPosition 0 ii after beginTransaction called always true until abortTransaction called commitTransaction called under variant buffer length bufferPosition Ces exemples montrent comment la syntaxe abstraite de JTPL est concr tement enrichie par les balises et de d but et de fin de pr dicat JML et par le marqueur de fin de propri t La premi re formule signifie qu apr s after la fin d une transaction par validation commit ou par rollback abort et avant before qu une autre transaction ne commence le buffer doit toujours always tre vide C est une propri t de s ret quelque chose de mauvais ne doit pas arriver La seconde formule signifie qu apr s after qu une transaction ait commenc elle doit fatalement until se terminer par un rollback ou une validation Pour cette seconde formule qui est une vivacit quelque chose de bon doit n cessairement arriver on doit de plus fourn
29. re directement en un ensemble d annotations JML C est pourquoi nous mettons la disposition du sp cifieur des langages compacts pour exprimer de telles propri t s et un m canisme de traduction automatique de ces propri t s en annotations JML directement ins r es dans le code de la classe v rifier 3 Comment formaliser des propri t s de s curit Nous proposons ici un langage de formules temporelles et une structure d automates pour formaliser des propri t s de s curit L un et l autre sont issus d une analyse des besoins les plus fr quents des d veloppeurs Java en mati re d expression de la s curit de leur code Chaque formalisme est illustr par des exemples de propri t s pour la classe APDU 3 1 Des sch mas pour exprimer les propri t s Afin d aider les programmeurs Java crire des annotations JML Trentelman et Huisman 26 ont propos une extension temporelle de JML inspir e des sch mas de sp cification Specification Pattern 12 du projet Bandera Une des motivations de ce projet tait d aider le sp cifieur crire des propri t s temporelles en lui fournissant des sch mas pour les propri t s les plus courantes A travers une tude de plus de 500 exemples de sp cifications M Dwyer et son quipe ont montr que 80 des besoins de sp cification pouvaient tre couverts par un nombre restreint de sch mas de propri t Le langage d fini par Huisman et Trentelman q
30. se avec des annotations JML 21 Java Modeling Language Il s agit de toutes les lignes pr c d es par et de tous les blocks d limit s par et Les annotations JML avant l ent te des m thodes Java permettent d en d crire le comportement Ces annotations formalisent une partie des informations donn es en langue naturelle dans la documentation HTML de la classe APDU Les principales annotations JML sont des invariants clause invariant d crivant une propri t que tous les tats visibles de la classe doivent v rifier des pr conditions de m thode clause requires et des post conditions de m thode clause ensures qui indiquent une propri t qui doit tre vraie quand la m thode se termine Les tats visibles sont les tats pr c dant l appel d une m thode de la classe et les tats de terminaison des m thodes de la classe Les pr dicats JML suivent la syntaxe des expressions bool ennes Java tendue avec des mots clefs sp cifiques JML comme old qui fait r f rence la valeur d une variable dans l tat visible pr c dent Des variables JML ghost peuvent tre d clar es et mises jour clauses set Le mot clef pure permet de sp cifier qu une m thode est sans effet de bord De telles m thodes peuvent tre utilis es l int rieur d un pr dicat JML package javacard framework normal_behavior public class APDU requires bOff len lt getBuffer length inv
31. t partir de laquelle elles ont t g n r es Les tapes de la g n ration d annotations avec l interface graphique de l outil JAG sont les suivantes 1 Chargement de l outil L outil JAG s ouvre sur une interface principale pr sent e dans la figure 9 2 S lection du fichier d entr e En cliquant simplement sur le bouton Choose Input File Choisir un fichier d entr e une bo te de dialogue s ouvre afin de choisir un fichier Java Le fichier est alors analys et un contr le de type est r alis nous utilisons pour cela l analyseur syntaxique fourni par les JMLTools Si le fichier ne comporte pas d erreur de syntaxe il est affich dans le cadre 1 3 S lection du fichier contenant les propri t s temporelles En cliquant sur le bouton Choose Property File choisir un fichier de propri t on ouvre une bo te de dialogue qui permet de s lectionner le fichier de propri t s temporelles Apr s analyse syntaxique la liste des propri t s est affich e dans le cadre central 2 Les primitives ainsi que les annotations 85 Giorgetti amp Groslambert ghost public boolean gt buffer length bufferPosition gTLbeginTransactioncalled_2 false lt old buffer length bufferPosition ghost public boolean gTLcommitTransactionterminates_1 false ghost public boolean gTLabortTransactionterminates_1 false constraint old gTLbeginTrans
32. t de valider la propri t soit d exhiber un contre exemple 4 4 R sultats exp rimentaux L outil a t valid sur diff rentes classes Java dont la classe APDU pr sent e dans cet article Une tude plus importante a t r alis e sur un porte monnaie lectronique pour la Java Card L outil JAG a t utilis pour v rifier des propri t s temporelles de s ret et de vivacit sur la sp cification JML de ce porte monnaie Sur cette sp cification constitu e de 500 lignes de JML Voutil JAG a g n r des annotations suppl mentaires pour v rifier des propri t s d unicit de la personnalisation de la carte et d atomicit d op rations d compos es en plusieurs m thodes Ensuite la v rification de la consistance des annotations g n r es vis vis du mod le JML a t r alis e l aide de l outil JML2B 4 3 un g n rateur d obligations de preuve de consistance des mod les JML bas sur une traduction vers B Certaines des obligations de preuve g n r es partir des annotations suppl mentaires ont d tre prouv es de mani re interactive La table 1 r sume les r sultats obtenus en utilisant les outil Jack 9 et JML2B pour le mod le JML du porte monnaie electronique pour g n rer et v rifier en aval les obligations de preuve OP 83 Giorgetti amp Groslambert Nom de l exemple Nombre de propri t s tem Nombre d annotations g Nombre d OP dont auto porelles v rif
33. te cette traduction premi re tape pour v rifier que le code Java est conforme ces propri t s de s curit Le mode d emploi de cet outil est donn dans la partie 5 Enfin la partie 6 conclut et pr sente des perspectives de travaux futurs Partiellement financ par PACI SI GECCOO 76 Un programme annot en vaut deux 2 Exemple applicatif et pr sentation de JML La figure 1 pr sente un extrait de la classe javacard framework APDU de la plateforme Java Card 2 1 Cette classe fait partie de PAPI Application Programming Interface Java Card d finie par Sun Microsystems Son interface est d crite dans sa documentation au format javadoc mais son code source n est pas diffus Le JCRE Java Card Runtime Environment utilise une instance de la classe APDU Application Protocol Data Unit comme support de communication entre la carte puce et les terminaux qui l accueillent Plus pr cis ment l information est lue et crite dans le buffer de APDU La m thode getBuffer permet d acc der a ce buffer Les donn es chang es pouvant tre plus longues que la capacit du buffer la classe APDU est organis e en m thodes qui fragmentent leur transfert Ainsi les m thodes setIncomingAndReceive et receiveBytes collaborent leur r ception tandis que les m thodes setOutgoing et sendBytes organisent la r ponse de la carte Dans la figure 1 nous avons enrichi l interface de la clas
34. tinence de leurs remarques qui leur ont permis d am liorer la qualit de ce document R f rences 1 M Barnett K Rustan M Leino and Wolfram Schulte The Spec programming system An overview In CASSIS 2004 LNCS Springer 2004 2 F Bellegarde J Groslambert M Huisman J Julliand and O Kouchnarenko Verification of liveness properties with JML Technical Report RR 5331 INRIA 2004 3 F Bouquet F Dadeau and J Groslambert Checking JML specifications with B machines In H Treharne S King M Henson and S Schneider editors Procs of the Int Conf on Formal Specification and Development in Z and B ZB 05 volume 3455 of LNCS pages 435 454 Guildford Uk April 2005 Springer F Bouquet F Dadeau and J Groslambert JML2B Checking JML specifications with B machines In B 2007 the 7th Int B Conference Tool Session volume 4355 of LNCS pages 285 288 Besancon France January 2007 Springer 4 5 F Bouquet F Dadeau J Groslambert and J Julliand Safety property driven test generation from JML specifications In FATES RV 06 1st Int Workshop on Formal Approaches to Testing and Runtime Verification volume 4262 of LNCS pages 225 239 Seattle WA USA August 2006 Springer 6 F Bouquet F Dadeau and B Legeard Automated boundary test generation from JML specifications In FM 06 14th Int Conf on Formal Methods volume 4085 of LNCS pages 428 443 Hamilton
35. ue nous proposons de nommer JTPL pour Java Temporal Pattern Language langage de sch mas temporels pour Java suit l approche des sch mas de sp cification de Dwyer L une de ses sp cificit s est de tenir compte de la terminaison exceptionnelle de Java qui survient lorsque l ex cution d un programme Java l ve une exception qui peut ventuellement tre captur e pour poursuivre l ex cution du programme Nous verrons comment le langage JTPL permet d exprimer facilement des propri t s relatives ces lev es d exception La s mantique formelle de ce langage est d taill e dans 26 ainsi que la traduction des propri t s de s ret La traduction des propri t s de vivacit est expliqu e dans 2 3 1 1 Pr sentation du langage Dans cette partie nous pr sentons informellement le langage JTPL Celui ci est bas sur la notion de propri t d tat Une propri t d tat est un pr dicat JML m enabled ou m not enabled ot m d signe une m thode Java de la classe La structure m enabled resp not enabled d finit implicitement l ensemble des tats partir desquels une invocation de la m thode m ne d clenchera pas d exception resp d clenchera obligatoirement une exception Chaque propri t d tat P doit tre encapsul e dans une propri t de trace qui peut tre always P eventually P ou encore la conjonction ou la disjonction de deux propri t s de trace La s mantique de ces propri t s de tr
36. ystem final int LENGTH 30 byte status new byte LENGTH byte buffer new byte LENGTH int bufferPosition 0 4 invariant buffer null invariant buffer length LENGTH Y P invariant butterPosition lt LENGTH 88 5 2 after beginTransaction alled always true until abortTransaction called omrmitTransaction called inder_invariant true ariant buffer length bufferPosition Utilisation de l interface graphique TransactionSystemJTPL java package jtpl java jml ts import java lang import org jmispecs lang public class TransactionSystemJTPL extends java lang Object invariant buffer null invariant buffer length LENGTH invariant bufferPosition LENGTH amp amp bufferPosition gt 0 private invariant gTLbeginTransactioncalled_0 gt true 4 private invariant gTLbeginTransactioncalled_0 gt true F1G 9 Interface principale de JAG L outil JAG dispose d une interface graphique repr sent e dans la figure 9 Elle permet de s lectionner et de visualiser les fichiers de travail La fen tre principale est compos e de trois parties a gauche une fen tre permet de consulter le fichier source au centre apparait la liste des propri t s temporelles v rifier enfin droite on peut visualiser le fichier de sortie g n r Les annotations ajout es par l outil apparaissent de la m me couleur que la propri

le pdf - JFLA

Contents

Download Pdf Manuals

Related Search

Related Contents