{"id":4376,"date":"2014-07-15T06:00:37","date_gmt":"2014-07-15T04:00:37","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4376"},"modified":"2014-07-14T17:50:18","modified_gmt":"2014-07-14T15:50:18","slug":"resena-from-operational-models-to-information-theory-side-channels-in-pgcl-with-isabelle","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-from-operational-models-to-information-theory-side-channels-in-pgcl-with-isabelle\/","title":{"rendered":"Rese\u00f1a: From operational models to information theory; side channels in pGCL with Isabelle"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle<\/a> titulado <a href=\"http:\/\/bit.ly\/1qTt9uo\">From operational models to information theory; side channels in pGCL with Isabelle<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/www.cse.unsw.edu.au\/~davec\">David Cock<\/a> (del <em>Software Systems Research Group, NICTA<\/em>).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  <em>In this paper, we formally derive the probabilistic security predicate (expectation) for a guessing attack against a system with side-channel leakage, modelled in pGCL. Our principal theoretical contribution is to link the process-oriented view, where attacker and system execute particular model programs, and the information-theoretic view, where the attacker solves an optimal-decoding problem, viewing the system as a noisy channel. Our practical contribution is to illustrate the selection of probabilistic loop invariants to verify such security properties, and the demonstration of a mechanical proof linking traditionally distinct domains.<\/em>\n<\/p><\/blockquote>\n<p>El trabajo se present\u00f3 ayer en el <a href=\"http:\/\/www.cs.uwyo.edu\/~ruben\/itp-2014\">ITP 2014<\/a> (<em>5th Conference on Interactive Theorem Proving<\/em>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle\/HOL se encuentra <a href=\"http:\/\/afp.sourceforge.net\/entries\/pGCL.shtml\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle titulado From operational models to information theory; side channels in pGCL with Isabelle. Su autor es David Cock (del Software Systems Research Group, NICTA). Su resumen es In this paper, we formally derive the probabilistic security predicate (expectation) for a guessing attack against a system&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[144,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4376"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4376"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4376\/revisions"}],"predecessor-version":[{"id":4377,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4376\/revisions\/4377"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4376"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4376"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4376"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}