{"id":111852,"date":"2018-03-11T10:38:33","date_gmt":"2018-03-11T10:38:33","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/abstract-certification-of-java-programs-in-rewriting-logic\/"},"modified":"2018-03-11T10:38:33","modified_gmt":"2018-03-11T10:38:33","slug":"abstract-certification-of-java-programs-in-rewriting-logic","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/lenguajes-de-programacion\/abstract-certification-of-java-programs-in-rewriting-logic\/","title":{"rendered":"Abstract certification of java programs in rewriting logic"},"content":{"rendered":"

Tesis doctoral de Mauricio Fernando Alba Castro <\/strong><\/h2>\n

In this thesis we propose an abstraction based certification technique for java programs which is based on rewriting logic, a very general logical and semantic framework efficiently implemented in the functional programming language maude. We focus on safety properties, i.E. Properties of a system that are defined in terms of certain events not happening, which we characterize as unreachability problems in rewriting logic. The safety policy is expressed in the style of jml, a standard property specification language for java modules. in order to provide a decision procedure, we enforce finite-state models of programs by using abstract interpretation. starting from a specification of the java semantics written in maude, we develop an abstraction based, finite-state operational semantics also written in maude which is appropriate for program verification. as a by-product of the verification based on abstraction, a dependable safety certificate is delivered which consists of a set of rewriting proofs that can be easily checked by the code consumer by using a standard rewriting logic engine. The abstraction based proof-carrying code technique, called javapcc, has been implemented and successfully tested on several examples, which demonstrate the feasibility of our approach. we analyse local properties of java methods: i.E. Properties of methods regarding their parameters and results. We also study global confidentiality properties of complete java classes, by initially considering non–interference and, then, erasure with and without non–interference. Non–interference is a semantic program property that assigns confidentiality levels to data objects and prevents illicit information flows from occurring from high to low security levels. In this thesis, we present a novel security model for global non–interference which approximates non–interference as a safety property. Erasure is a way of strengthening confidentiality by upgrading data confidentiality levels, up to the extreme of demanding the removal of secret data from the system. in this thesis, we also propose a certification technique for confidentiality of complete java classes that includes non–interference and erasure policies.<\/p>\n

 <\/p>\n

Datos acad\u00e9micos de la tesis doctoral \u00abAbstract certification of java programs in rewriting logic<\/strong>\u00ab<\/h3>\n
    \n
  • T\u00edtulo de la tesis:<\/strong>\u00a0 Abstract certification of java programs in rewriting logic <\/li>\n
  • Autor:<\/strong>\u00a0 Mauricio Fernando Alba Castro <\/li>\n
  • Universidad:<\/strong>\u00a0 Polit\u00e9cnica de Valencia<\/li>\n
  • Fecha de lectura de la tesis:<\/strong>\u00a0 24\/11\/2011<\/li>\n<\/ul>\n

     <\/p>\n

    Direcci\u00f3n y tribunal<\/h3>\n
      \n
    • Director de la tesis<\/strong>\n
        \n
      • Mar\u00eda Alpuente Frasnedo<\/li>\n<\/ul>\n<\/li>\n
      • Tribunal<\/strong>\n
          \n
        • Presidente del tribunal: salvador Lucas alba <\/li>\n
        • ricardo Pe\u00f1a mar\u00ed (vocal)<\/li>\n
        • Francisco Javier Duran mu\u00f1oz (vocal)<\/li>\n
        • claude March\u00e9 (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n

           <\/p>\n","protected":false},"excerpt":{"rendered":"

          Tesis doctoral de Mauricio Fernando Alba Castro In this thesis we propose an abstraction based certification technique for java programs […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"footnotes":""},"categories":[13880,6474,16820,15624,30772],"tags":[217764,66541,6479,222735,16545,45326],"class_list":["post-111852","post","type-post","status-publish","format-standard","hentry","category-informatica","category-lenguajes-de-programacion","category-politecnica-de-valencia","category-software","category-teoria-de-lenguajes-formales","tag-claude-marche","tag-francisco-javier-duran-munoz","tag-maria-alpuente-frasnedo","tag-mauricio-fernando-alba-castro","tag-ricardo-pena-mari","tag-salvador-lucas-alba"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/111852","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/comments?post=111852"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/111852\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=111852"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=111852"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=111852"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}