{"id":1041,"date":"2018-05-25T11:52:52","date_gmt":"2018-05-25T09:52:52","guid":{"rendered":"https:\/\/samovar2022.int-evry.fr\/index.php\/2018\/05\/25\/seminaire-samovar-r3s-presente-par-emilio-j-gallego-arias-le-5-06-2018-en-g09\/"},"modified":"2020-09-04T18:45:46","modified_gmt":"2020-09-04T16:45:46","slug":"seminaire-samovar-r3s-presente-par-emilio-j-gallego-arias-le-5-06-2018-en-g09","status":"publish","type":"post","link":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/2018\/05\/25\/seminaire-samovar-r3s-presente-par-emilio-j-gallego-arias-le-5-06-2018-en-g09\/","title":{"rendered":"S\u00e9minaire SAMOVAR\/R3S pr\u00e9sent\u00e9 par Emilio J. Gallego-Arias, le 5\/06\/2018 en G09"},"content":{"rendered":"<p><strong>Title:<\/strong>  Towards formally-verified Solidity specifications<\/p>\n<p><strong>Quand: <\/strong> le mardi 05 juin 2018 \u00e0 14h00<br \/>\n<strong>O\u00f9:<\/strong> Salle G09, T\u00e9l\u00e9com SudParis, Evry.<\/p>\n<p><strong>Abstract<\/strong>: In the last few years, permission-less distributed execution platforms have gained enormous popularity, as they have become a computing environment of choice for decentralized asset management.  Concretely, the Ethereum project implements a distributed ledger featuring a Turing-complete execution engine with read\/write capability to the underlying blockchain-based storage. Thus, users can immutably store and interact with other \u00ab\u00a0smart contracts\u00a0\u00bb, which has allowed the development of rich trustless applications. However, lack of central control does come at a prize: once a contract is deployed to the blockchain, its code is in principle immutable, thus bugs take a very different dimension as the same autonomy that makes the permissionless setting interesting works against the effective mitigation of vulnerabilities.<br \/>\nWe aim to improve this situation with the introduction of Consolidity, a formal semantics and compiler for a subset of the Solidity programming language; Consolidity&rsquo;s formal semantics provide a principled basis for the formal reasoning about high-level properties of given contracts, and allow us to define a specification language formally capturing the intent of ERCs. Contrary to other works in the smart contracts verification arena, Consolidity targets the widely-used Solidity language in an attempt to both reach a larger number of users and to gain a deeper understanding of real-world Ethereum platform use.<br \/>\nIn the talk, we will review the basics of the Ethereum execution platform: the EVM, and of the Solidity programming language. We will discuss a few example smart contracts that make interesting targets for the verification of high-level properties. Then, we will present our semantics for Solidity, and use it to formally model some key properties under realistic assumptions on consensus and transaction fairness. In particular we will address the core of the ERC 20 and ERC 721 standards, and strategy proofness for a smart contract implementing an energy market.<\/p>\n<p><strong>Short Bio:<\/strong> Emilio is a postdoctoral researcher at the CRI, MINES ParisTech. He works on formal semantics of Digital Signal Processing and interactive theorem proving. He likes to code in a variety of functional programming languages, including Coq, OCaml, and Haskell; and enjoys contributing to research open source projects.  Previously, he was a postdoctoral appointee in the privacy group of the University of Pennsylvania working on privacy, security, software verification, and semantics. He holds a PhD from the Technical University of Madrid on the categorical and relational semantics of constraint logic programming.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Title: Towards formally-verified Solidity specifications Quand: le mardi 05 juin 2018 \u00e0 14h00 O\u00f9: Salle G09, T\u00e9l\u00e9com SudParis, Evry. Abstract: In the last few years, permission-less distributed execution platforms have gained enormous popularity, as they have become a computing environment of choice for decentralized asset management. Concretely, the Ethereum project implements a distributed ledger featuring [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":1040,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"ocean_post_layout":"","ocean_both_sidebars_style":"","ocean_both_sidebars_content_width":0,"ocean_both_sidebars_sidebars_width":0,"ocean_sidebar":"","ocean_second_sidebar":"","ocean_disable_margins":"enable","ocean_add_body_class":"","ocean_shortcode_before_top_bar":"","ocean_shortcode_after_top_bar":"","ocean_shortcode_before_header":"","ocean_shortcode_after_header":"","ocean_has_shortcode":"","ocean_shortcode_after_title":"","ocean_shortcode_before_footer_widgets":"","ocean_shortcode_after_footer_widgets":"","ocean_shortcode_before_footer_bottom":"","ocean_shortcode_after_footer_bottom":"","ocean_display_top_bar":"default","ocean_display_header":"default","ocean_header_style":"","ocean_center_header_left_menu":"","ocean_custom_header_template":"","ocean_custom_logo":0,"ocean_custom_retina_logo":0,"ocean_custom_logo_max_width":0,"ocean_custom_logo_tablet_max_width":0,"ocean_custom_logo_mobile_max_width":0,"ocean_custom_logo_max_height":0,"ocean_custom_logo_tablet_max_height":0,"ocean_custom_logo_mobile_max_height":0,"ocean_header_custom_menu":"","ocean_menu_typo_font_family":"","ocean_menu_typo_font_subset":"","ocean_menu_typo_font_size":0,"ocean_menu_typo_font_size_tablet":0,"ocean_menu_typo_font_size_mobile":0,"ocean_menu_typo_font_size_unit":"px","ocean_menu_typo_font_weight":"","ocean_menu_typo_font_weight_tablet":"","ocean_menu_typo_font_weight_mobile":"","ocean_menu_typo_transform":"","ocean_menu_typo_transform_tablet":"","ocean_menu_typo_transform_mobile":"","ocean_menu_typo_line_height":0,"ocean_menu_typo_line_height_tablet":0,"ocean_menu_typo_line_height_mobile":0,"ocean_menu_typo_line_height_unit":"","ocean_menu_typo_spacing":0,"ocean_menu_typo_spacing_tablet":0,"ocean_menu_typo_spacing_mobile":0,"ocean_menu_typo_spacing_unit":"","ocean_menu_link_color":"","ocean_menu_link_color_hover":"","ocean_menu_link_color_active":"","ocean_menu_link_background":"","ocean_menu_link_hover_background":"","ocean_menu_link_active_background":"","ocean_menu_social_links_bg":"","ocean_menu_social_hover_links_bg":"","ocean_menu_social_links_color":"","ocean_menu_social_hover_links_color":"","ocean_disable_title":"default","ocean_disable_heading":"default","ocean_post_title":"","ocean_post_subheading":"","ocean_post_title_style":"","ocean_post_title_background_color":"","ocean_post_title_background":0,"ocean_post_title_bg_image_position":"","ocean_post_title_bg_image_attachment":"","ocean_post_title_bg_image_repeat":"","ocean_post_title_bg_image_size":"","ocean_post_title_height":0,"ocean_post_title_bg_overlay":0.5,"ocean_post_title_bg_overlay_color":"","ocean_disable_breadcrumbs":"default","ocean_breadcrumbs_color":"","ocean_breadcrumbs_separator_color":"","ocean_breadcrumbs_links_color":"","ocean_breadcrumbs_links_hover_color":"","ocean_display_footer_widgets":"default","ocean_display_footer_bottom":"default","ocean_custom_footer_template":"","ocean_post_oembed":"","ocean_post_self_hosted_media":"","ocean_post_video_embed":"","ocean_link_format":"","ocean_link_format_target":"self","ocean_quote_format":"","ocean_quote_format_link":"post","ocean_gallery_link_images":"on","ocean_gallery_id":[],"footnotes":""},"categories":[316],"tags":[],"class_list":["post-1041","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-seminaires-r3s-2018-fr","entry","has-media"],"_links":{"self":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/posts\/1041","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/comments?post=1041"}],"version-history":[{"count":1,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/posts\/1041\/revisions"}],"predecessor-version":[{"id":1530,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/posts\/1041\/revisions\/1530"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/media\/1040"}],"wp:attachment":[{"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/media?parent=1041"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/categories?post=1041"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/samovar.telecom-sudparis.eu\/index.php\/wp-json\/wp\/v2\/tags?post=1041"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}