| Keynotes Sessions | ||
Liana Hadarean (Amazon) |
Elvira Albert (UCM) |
Franjo Ivančić (Google) |
Liana Hadarean
One-click formal methods ( Summary)
Formal methods have been successfully applied in domains such as microprocessor hardware design and aerospace. However, despite 50 years of research and development, we have not seen wide adoption of formal methods for large and complex systems such as web services, industrial automation, or enterprise support software. One of the key difficulties when proving security, safety, and robustness of these systems is the problem of finding the models of system architectures necessary for analysis. Additionally, the size of the potential user community and the business value typically does not justify the creation of scalable and easy-to-use tools for formal verification. With the cloud, much of this has changed. Descriptions of cloud services provide accurate models in the form of computer-readable contracts. These contracts establish and govern how the system behaves and in many cases these models are amenable to formal analysis at scale. Most importantly, since those models are used by a large user community, it is now economically feasible to build the tools needed to verify those models. In this talk, we discuss the trend of constructing practical and scalable cloud-based formal methods at Amazon Web Services and how they can easily be used by customers – sometimes with just one-click.
Liana Hadarean is a Senior Applied Scientist on the CodeGuru team at Amazon Web Services. She is currently working on developing a sound static analyzer for Java code. Before joining Amazon, she worked at Synopsys as one of the developers of the Coverity Static Analysis tool. Liana received her PhD from New York University, where her research focused on Satisfiability Modulo Theories (SMT) and she was one of the developers of the CVC4 SMT solver. Her research interests are in the field of formal methods, static analysis and automated reasoning and applying these techniques at scale.
Elvira Albert
Smart – and also reliable and gas-efficient – Contracts
Smart contracts are a very interesting application domain for validation, verification and optimization techniques since (1) they are relatively small in size, hence the application of these techniques scales well, (2) they are valuable (in the corresponding blockchain cryptocurrency), hence software bugs or inefficiencies can cause economical losses, and (3) they require proving new properties to ensure their reliability and efficiency. This talk overviews the main features of smart contracts and discusses our current work on the verification of gas-related and safety properties whose main goals are to save resources, prevent vulnerabilities and avoid potential attacks.
Elvira Albert is a Professor at the Complutense University of Madrid, Spain. She has many years of experience developing validation and verification tools for checking that a software product meets the given requirements or specifications and it thus fulfills its intended behaviour. Over the past two years, she has been investigating on the extension and application of validation and verification techniques to ensure the reliability and efficiency of smart contracts that run on the Ethereum Virtual Machine. She currently leads a large research group, the COSTA team, made up of eight senior researchers and six PhD students. She is author of around 130 publications in international journals and volumes strongly related to the topics of validation and verification of sequential and concurrent programs. Elvira has been recently appointed as Area Editor for the area of Specification, Analysis and Verification of Systems of the TPLP journal and as program co-chair of the next edition of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2020).
Franjo Ivančić
SunDew: Systematic Automated Security Testing
At Google, we have found tens of thousands of security and robustness bugs by fuzzing C and C++ libraries. This talk covers the various aspects of one of the projects working on automated scalable techniques related to fuzzing at Google: how to fuzz, what to fuzz, and how to deal with discovered bugs. First, we present a distributed fuzzing infrastructure that allows us to cooperatively utilize multiple test generation techniques. Then, this talk will describe our FUDGE system for automated fuzz driver generation, which automatically generates fuzz driver candidates for libraries based on existing client code. Running large-scale fuzzing services also causes lots of bugs and vulnerabilities to be reported. This talk describes various techniques to provide feedback to developers to reduce the time a known security bug remains open. Finally, this talk will also highlight challenges and opportunities to incorporate security testing into the general software development workflow.
Franjo is a Staff Software Engineer at Google in New York focusing on application security, program analysis and software development productivity tools. Prior to joining Google, he was a Senior Researcher at NEC Labs in the Systems Analysis and Verification group in Princeton, NJ. He received a Ph.D. in Computer and Information Science from the University of Pennsylvania in Philadelphia, PA, on modeling and verification of cyber-physical systems.