STINT Workshop on Assured Software Engineering

STINT Workshop on Assured Software Engineering

This workshop is in the context of the STINT project "Runtime Monitoring of Unmanned Aerial Vehicles" awarded to researchers of University of Gothenburg and University of Buenos Aires. 

The workshop will cover the broad area of assured software engineering, that is techniques and methods that allow reasoning and analysing software engineering artifacts to provide greater assurance about the correctness of the software under development. 

The workshop brings together researchers based in Sweden and Argentina working in this area. 

Talks will be in Spanish and are open to the general public. 

IMPORTANTE: Todas las charlas son en castellano. 

Programa

Apertura e Introducciones:  10:00 - 10:30

Sesión 1: 10:30 - 12:00

Alejandro Russo, Chalmers University (Suecia). DPella: Un framework de programación para Privacidad Diferencial con Exactitud

Nazareno Aguirre, UNRC/CONICET, Mejoramiento de Ejecución Simbólica Generalizada usando SAT. 

Juan Pablo Galeotti, ICC, UBA/CONICET: Desafíos y oportunidades en Generación Automática de Casos de Tests.

Sesión 2: 13:30 - 15:00

Gerardo Schneider, Chalmers University (Suecia), Smart Contracts: Qué son? Temas abiertos y vínculo con el mundo real.

Diego Garbervetsky, ICC, UBA/CONICET, Integración de Herramientas Automáticas en Auditorías de Smart Contracts.

Marcelo Frias,  ITBA/CONICET: Título a confirmar, pero será seguramente sobre verificación automática de código. 

Sesión 3: 15:30 - 17:00

Pablo Castro, UNRC/CONICET, Midiendo Tolerancia Fallas por Enmascaramiento.

Carlos Lopez Pombo, ICC, UBA/CONICET: Sistemas distribuidos reconfigurables basados en servicios.

Sebastian Uchitel, ICC, UBA/CONICET: Síntesis automática de planes reactivos. Aplicaciones en robótica. 

Detalle de Charlas

Pablo Castro. Midiendo Tolerancia Fallas por Enmascaramiento     

In this talk we introduce a notion of fault-tolerance distance between labeled transition systems. Intuitively, this notion of distance measures the degree of fault-tolerance exhibited by a candidate system. In practice, there are different kinds of fault-tolerance,  we restrict ourselves to the analysis of masking fault-tolerance because it is often a highly desirable goal for critical systems. Roughly speaking, a system is masking fault-tolerant when it is able to completely mask the faults, not allowing these faults to have any observable consequences for the users. We capture masking fault-tolerance via a simulation relation, which is accompanied by a corresponding game characterization. We enrich the resulting games with quantitative objectives to define the notion of masking fault-tolerance distance. Furthermore, we investigate the basic properties of this notion of masking distance, and we prove that it is a directed semimetric. We have implemented our approach in a prototype tool that automatically computes the masking distance between a nominal system and a fault-tolerant version of it. We have used this tool to measure the masking tolerance of multiple instances of several case studies.

Pablo Castro es Investigador Adjunto del CONICET y Profesor Adjunto de la UNRC. Obtuvo su titulo de Dr en la Universidad de McMaster (Ontario, Canada) bajo la dirección de Tom Maibaum en 2010. Sus temas de investigación incluyen métodos formales, teoría de categorías aplicada a la ingeniería de software, aplicaciones de lógicas modales y deónticas para la verificación de sistemas. Forma parte de diversos proyectos de investigación sobre estas temáticas, y publica regularmente en revistas y conferencias reconocidas en estas áreas.

Alejandro Russo. DPella: A programming framework for Differential Privacy with Accuracy

Differential privacy offers a formal framework for reasoning about privacy and accuracy of computations on private data. It also offers a rich set of building blocks for constructing data analyses. When carefully calibrated, these analyses simultaneously guarantee privacy of the individuals contributing their data and accuracy of their results for inferring useful properties about the population. One important building block for differential privacy are composition theorems, which allow multiple differentially private data analyses to be composed together with a graceful degradation of the privacy and accuracy parameters. The compositional nature of differential privacy has motivated the design and implementation of several programming languages aimed at helping a data analyst in programming differentially private data analyses. However, most of the programming languages for differential privacy proposed so far provide support for reasoning about privacy but not for reasoning about accuracy of data analyses. To overcome this limitation, in this work we present DPella, a programming framework providing data analysts with support for reasoning about privacy, accuracy and their trade-offs. DPella is implemented as a domain specific language in the functional programming language Haskell. The distinguished feature of DPella is a novel component which statically tracks the accuracy of different data analyses. In order to make tighter accuracy estimations, this component leverages information-flow control techniques, in the form of taint analysis, for automatically inferring statistical independence of the different noise quantities added for guaranteeing privacy. We show the flexibility of our approach by implementing classical counting queries (e.g., CDFs) found in the literature and how DPella exposes the trade-offs between privacy and accuracy. Furthermore, we use DPella to analyze hierarchical counting queries (like those done by Census Bureaus), where accuracy have different constrains per level and data analysts should figure out the best manner to trade-off privacy to meet the accuracy requirements.

Alejandro Russo is a professor at Chalmers University of Technology working on the intersection of functional languages, security, and systems. His research ranges from foundational aspects of security to developing tools to secure software written in Haskell, Python, and JavaScript. Prof. Russo worked on prestigious research institutions like Stanford University, where he was appointed visiting associate professor back in 2013-2015.

Gerardo Schneider. Smart Contracts: What are they? Open Issues and Connection with the Real World

Los Contratos Inteligentes (Smart Contracts, en inglés) suelen definirse como un protocolo informático destinado a facilitar, verificar o hacer cumplir digitalmente la negociación o el cumplimiento de un acuerdo o “contrato”. Más concretamente, los contratos inteligentes son programas (software) ejecutados en la llamada blockchain. El hecho de ser ejecutados en la blockchain, garantiza que tales transacciones se ejecuten de forma “confiable”sin necesidad de intermediarios, permitiendo además que estas sean rastreables e irreversibles. De esta forma se disminuye la probabilidad de fraudes, y en caso de que existan, incrementa la posibilidad de detectarlos y de determinar culpables en caso de violaciones contractuales.

En esta charla introduciré smart contracts (a alto nivel), poniendo énfasis en el estado del arte, limitaciones y oportunidades, y la conexión de tales “contratos” con los contratos legales que tratan de representar.

Gerardo Schneider received a PhD degree in Computer Science from the University Joseph Fourier (thesis done at the VERIMAG lab), Grenoble (France), in 2002. From 2003 till 2009 he was a researcher at Uppsala University (Sweden), Irisa/INRIA Rennes (France), and the University of Oslo (Norway). 

He joined the Department of Computer Science and Engineering at the University of Gothenburg (Sweden) in July 2009, where he has been a full professor since July 2014. His research interests include formal verification (static and runtime verification, model checking, testing), the specification and analysis of normative documents, and privacy. (http://www.cse.chalmers.se/~gersch).

Nazareno Aguirre. Generalized Symbolic Execution improved by SAT

Symbolic execution allows one to systematically explore program paths, by executing programs on symbolic inputs, and constructing path conditions that can be analyzed using constraint solving. When programs handle complex heap-allocated data structures, and executions are assumed to begin in states satisfying a certain property like a precondition or invariant, symbolic execution is generalized to also deal with partially concrete heaps, that are increasingly concretized as symbolic execution progresses, and whose feasibility has to be determined, to deem a path realizable and continue execution. This task, known as lazy initialization (LI), works by exhaustively considering all possible concretizations of symbolic parts of a heap as they are first accessed, and discarding those that are deemed infeasible. 

In this talk, we will present a number of improvements over LI, that can soundly reduce the number of possible concretizations considered by the technique, using SAT. More precisely, SAT is used to further prune infeasible paths during symbolic execution by precomputing bounds via SAT solving, that remove infeasible cases according a given precondition, and by dynamically checking the feasibility of partially concrete heaps during execution against the corresponding path conditions and the given precondition. 

Nazareno Aguirre es Investigador Independiente del CONICET y Profesor Asociado del Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto. Obtuvo su título de Doctor en Ciencias de la Computación en King's College London, Londres, Reino Unido, en 2004. Sus campos de especialidad en investigación incluyen los fundamentos de la ingeniería de software, y técnicas formales de análisis automático de software. Publica regularmente en revistas y conferencias destacadas del área. Dirige el Grupo de Métodos Formales e Ingeniería de Software de la Universidad Nacional de Río Cuarto, y está involucrado en varios proyectos de investigación sobre enfoques formales a la Ingeniería de Software.

Juan Pablo Galeotti. Desafios y oportunidades en Generación Automática de Casos de Tests

En la actualidad existen varias herramientas de generación automática de tests, tanto académicas como industriales. No obstante, su utilización dista mucho de formar parte de la práctica cotidiana de las personas que desarrollan software. En esta charla haremos un breve racconto sobre las principales herramientas que han surgido en los últimos años y de los distintos desafios en su adopción

Juan Pablo Galeotti es Doctor de la Universidad de Buenos Aires en el área de Ciencias de la Computación. Es profesor adjunto en el Dpto. de Computación de FCEyN, UBA, e investigador Adjunto del Instituto de Ciencias de la Computación del CONICET. El Dr. Galeotti es miembro de los comités de programas de las conferencias y revistas de ingeniería de software más prestigiosas del mundo. Entre otros logros, obtuvo el ACM/IEEE ASE 2014 Distinguished Paper Award por su trabajo "Automated Unit Test Generation for Classes with Environment Dependencies". Además, ha obtenido el premio Google Latin America Research Award 2017 y 2018 por sus aportes al campo de testing de aplicaciones Android.

Carlos Lopez Pombo. Sistemas distribuidos reconfigurables basados en servicios

Los nuevos paradigmas de computación Cloud/Fog, como así también la Internet de las cosas, han impulsado lo que hoy se denomina economía de las APIs. La idea que subyace es la posibilidad de construir nuevos servicios utilizando APIs provistas por terceras partes y, a su vez, hacer disponibles estos nuevos servicios publicando sus propias APIs. Una de las grandes promesas de la economía de las APIs es proveer medios que, entre otras cosas, permitan ayudar a las personas en sus actividades diarias, especialmente, automatizando interacciones business-to-business. Las aplicaciones y los dipositivos están cada vez más interconectados para poder asistir a las personas, por lo cual requerimientos tales como self-adaptiveness y reconfiguración dinámica son requerimientos esenciales de las aplicaciones actuales. En el modelos de las API, se vuelven cada vez más presentes los microservicios, donde se desplaza el desarrollo tradicional de software monolítico para dar lugar al uso de interfaces que permiten acceder a servicios y recursos distribuidos. De esta manera, las APIs posibilitan a los proveedores de software controlar cuáles son los aspectos de sus plataformas que desean hacer públicos y cuáles privados, posibilitando de esta manera la interoperabilidad. 

Llevar a la práctica este paradigma solo es plausible en la medida que contemos con lenguajes que acompañen el proceso de desarrollo de software que tengan la capacidad de expresar los SLAs declarando: a) las condiciones de interoperabilidad entre servicios, b) los requerimientos funcionales como condiciones sobre los valores intercambiados a través de los canales de comunicación, y c) los requerimientos no-funcionales como condiciones sobre variables cuantificables que reflejen métricas de calidad sobre los servicios. El ideal detrás de este paradigma se apoya en la capacidad real que tenga el middleware de realizar las tareas relativas al establecimiento de Service Level Agreements en forma completamente autónoma; particularidad que necesariamente prescribe que todo análisis de contratos, sean estos de interoperabilidad, funcionales o no-funcionales, se realice en forma automática.

En la charla visitaré los avances que hemos alcanzado y, muy especialmente, los trabajos que nos planteamos a futuro con la ambición de poner en práctica la construcción de brocker digital que pueda intervenir en forma autónomo en la llamada economía de las APIs.

Carlos Gustavo Lopez Pombo studied computer science in the School of Science at the University of Buenos Aires. He got a Ph.D. under the supervision of Prof. Marcelo Frías from the same institution. He specialized in topics related to foundations of heterogeneous and structured specifications, and applied logic and category theory in computer science, but also focused on the formal foundations and construction of tools providing tool support for effective software analysis and verification. Carlos G. Lopez Pombo is Professor at the University of Buenos Aires, was Associate Professor at McMaster University (Canada) until 2017, Associate Researcher of the Argentine Council for Science and Technical Research (CONICET), and member of the IFIP TC 1.3 – Foundations of software specification. 

Diego Garbervetsky - DC/ICC. FCEN. University of Buenos Aires 

Vera Bogdanich Espina - DC. FCEN. University of Buenos Aires / Open Zeppelin

Integrating automated tools into software audits 

In the last few years a plethora of tools for automatically analyzing smart contracts and highlighting potential vulnerabilities have appeared. Most of them are push-button tools that may uncover serious bugs but, unfortunately,  they also tend to report false positives (false bugs/issues) and false negatives (i.e., they missed issues). While many of them rely on a predefined set of patterns, leaving functional issues aside, approaches aiming at functional verification requires rich specifications (which can have errors as well) and the use of proof systems (sometimes requiring highly specialized human intervention). 

Together with  OpenZeppelin we started to research on how automated smart contract analysis tools can be integrated into the auditing process. In this talk we are going to report some of  the results of our use of state-of-the-art tools for smart contract analysis.  In particular, we will explore how tools could be leveraged to analyze the vulnerability of the MakerDAO voting mechanism recently disclosed by OpenZeppelin. (https://blog.zeppelin.solutions/technical-description-of-makerdao-governance-critical-vulnerability-facce6bf5d5e)

We argue that developers and auditors should be the ones playing a central role in the analysis of smart contracts. Thus, we believe software tools can and must empower them, but should not replace them.

Diego Garbervetsky is an Associated Professor and Deputy Head of the Computer Science Department in the University of Buenos Aires.  He also holds  research position in the National Council of Sciences (CONICET). He research focuses on automatic program analysis techniques aimed at program understanding, verification and validation. He regularly publishes and participes in program committees on the main conferences in Software Engineering. He is highly interested in technology transfer and has been participating in several collaboration project with the software industry.

Sebastian Uchitel. Síntesis automática de planes reactivos. Aplicaciones a robótica. 

La planificación automática es una rama de la inteligencia artificial que buscar resolver con garantías totales juegos de múltiples jugadores. Los sistemas adaptativos son sistemas que tienen la capacidad de reaccionar automáticamente a cambios en su entorno de ejecución, sus capacidades o sus objetivos más allá de si estos cambios fueron contemplados o imaginados en tiempo de diseño. En esta charla voy a dar una breve introducción a la planificación automática y explicar cómo pueden ser utilizada para el desarrollo de sistemas adaptativos, repasando una arquitectura de software para este tipo de sistemas, los desafíos técnicos que aún quedan por resolver y nuestras experiencias utilizando estas ideas en el dominio de la robótica. 

Sebastian Uchitel is a Full Professor at University of Buenos Aires, Principal Investigator at CONICET, and also holds a Readership at Imperial College London and is visiting professor at the National Institute of Informatics, Japan. He is currently Director of the UBA/CONICET Computer Science Research Insititute. He received his undergraduate Computer Science degree from University of Buenos Aires and his Phd in Computing from Imperial College London. His research interests are in behaviour modelling, analysis and synthesis applied to requirements engineering, software architecture and design, validation and verification, and adaptive systems. Dr. Uchitel was associate editor of the Transactions on Software Engineering and is currently associate editor of the Requirements Engineering Journal and the Science of Computer Programming Journal. He was program co-chair of ASE’06 and ICSE’10, and General Chair of ICSE’17. Dr Uchitel has been distinguished with the Philip Leverhulme Prize, ERC StG, the Konex Foundation Prize and the Houssay Prize.