The study of quantum computation has been motivated, in part, by the possibility that quantum computers can perform certain tasks dramatically faster than classical computers. Many of the known quantum-over-classical speedups, such as Shor’s algorithm for factoring integers and Grover’s search algorithm, can be framed as oracle problems or concept learning problems. In one model of concept learning, a student wishes to learn a concept from a teacher by making queries of the teacher. In the interest of efficiency, the student wishes to learn the concept by making as few queries as possible. For any such concept learning problem, there is a corresponding quantum concept learning problem. In the quantum version, the student is allowed to ask a superposition of queries – mathematically, a linear combination of queries – and the teacher answers with the corresponding superposition of the responses. After making this idea precise, we will examine several concept learning problems and their quantum analogues. We will discuss recent joint work with Daniel Copeland (UCSD), in which we show how tools from representation theory can be used to precisely analyze any quantum learning problem with sufficient symmetry.

Will also be streamed live on the Galois YouTube channel: https://www.youtube.com/channel/UC1TJ20iM_dCa0pq6h0tA79w

Abstract: Lean is an interactive theorem prover and functional programming language. Lean implements a version of the Calculus of Inductive Constructions. Its elaborator and unification algorithms are designed around the use of type classes, which support algebraic reasoning, programming abstractions, and other generally useful means of expression. Lean has parallel compilation and checking of proofs, and provides a server mode that supports a continuous compilation and rich user interaction in editing environments such as Visual Studio Code, Monaco, Emacs, and Vim. In the first part of this talk, we provide a short introduction to Lean, its applications, and its metaprogramming framework. We also describe how this framework extends Lean’s object language with an API to many of Lean’s internal structures and procedures, and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our implementation is efficient, and that it provides a convenient and flexible way of writing not only metaprograms and small-scale interactive tactics, but also more substantial kinds of automation. In the second part, we describe our plans for the system, and what we are currently working on.

More information about Lean can be found at http://leanprover.github.io. The interactive book “Theorem Proving in Lean” is the standard reference for Lean. The book is available in PDF and HTML formats. In the HTML version, all examples and exercises can be executed in the reader’s web browser.

Bio: I’m a Principal Researcher in the RiSE group at Microsoft Research. I joined Microsoft in 2006, before that I was a Computer Scientist at SRI International. I obtained my PhD at PUC-Rio in 2000. My research areas are automated reasoning, theorem proving, decision procedures, SAT and SMT. I’m the main architect of Lean, Z3, Yices 1.0 and SAL. Lean is an open source theorem prover and programming language. Sebastian Ullrich and I are currently developing the next version (Lean 4). Z3 and Yices are SMT solvers, and SAL (the Symbolic Analysis Laboratory) is an open source tool suite that includes symbolic and bounded model checkers, and automatic test generators. Z3 has been open sourced (under the MIT license) in the beginning of 2015. I received the Haifa Verification Conference Award in 2010. In 2014, the TACAS conference (Tools and Algorithms for the Construction and Analysis of Systems) has given an award for “The most influential tool paper in the first 20 years of TACAS” to the Z3 paper: Z3: An Efficient SMT Solver. 14th International Conference, TACAS 2008, vol. 4963 of Lecture Notes in Computer Science. In 2015, Z3 received the Programming Languages Software Award from ACM SIGPLAN. In 2017, the International Conference on Automated Deduction (CADE) presented the Skolem Award for my paper “Efficient E-Matching for SMT Solvers” that has passed the test of time, by being a most influential paper in the field. In 2018, the ETAPS conference has given the test of time award to the Z3 paper: Z3: An Efficient SMT Solver. You can see more about me at https://leodemoura.github.io/about.html

Abstract: In this talk, I’ll give a high-level overview of Penn’s Vellvm (Verified LLVM) project, which aims to build formal semantics in Coq for the LLVM IR. I’ll sketch some of our past results, in which we verified memory safety transformations and a variant of LLVM’s mem2reg optimization, focusing on the structure of the proof techniques. Along the way, I’ll highlight some of the challenges of reasoning about LLVM code (many of which are still open issues). I’ll wrap up with a status report about our ongoing efforts to re-engineer Vellvm as part of the DeepSpec NSF Expeditions project.

No experience with LLVM or Coq will be assumed.

Bio: I study programming languages and computer security. I have wide-ranging interests, and some of my most recent work touches on: Coq verification of LLVM program transformations and randomized algorithms, type-directed program synthesis, linear types and GUI programming. I have also spent a lot of time thinking about language-based enforcement of information-flow policies, low-level code memory safety, understanding dynamic security policies, and authorization logic. I am also interested in secure concurrent and distributed computing, functional programming languages, type theory, linear and modal logics, theorem proving and mechanized metatheory.

Title: New Applications of Software Synthesis: Firewall Repair and Verification of Configuration Files

Abstract: In this talk we present a systematic effort that can automatically repair firewalls, using the programming by example approach. Firewalls are widely employed to manage and control enterprise networks. Because enterprise-scale firewalls contain hundreds or thousands of policies, ensuring the correctness of firewalls – whether the policies in the firewalls meet the specifications of their administrators – is an important but challenging problem. In our approach, after an administrator observes undesired behavior in a firewall, she may provide input/output examples that comply with the intended behavior. Based on the given examples, we automatically synthesize new firewall rules for the existing firewall. This new firewall correctly handles packets specified by the examples, while maintaining the rest of the behavior of the original firewall.

We also show, using verification for configuration files, how to learn specification when the given examples is actually a set of configuration files. Software failures resulting from configuration errors have become commonplace as modern software systems grow increasingly large and more complex. The lack of language constructs in configuration files, such as types and grammars, has directed the focus of a configuration file verification towards building post-failure error diagnosis tools. In this talk we describe a framework which analyzes data sets of correct configuration files and derives rules for building a language model from the given data set. The resulting language model can be used to verify new configuration files and detect errors in them.

Bio: Ruzica Piskac is an assistant professor (tenure-track) at Yale, Computer Science Department. Her research interests span the areas of programming languages, software verification, automated reasoning, and code synthesis. A common thread in Ruzica's research is improving software reliability and trustworthiness using formal techniques. Ruzica has received a NSF CAREER award for her proposal, “Synthesis in a Live Programming Environment”. She proposed the concept of cooperative programming which combines a live programming environment and the programming by example paradigm.

Speaker:

Wouter Swierstra

Abstract:

Complex protocols describing the communication or storage of binary data are difficult to describe precisely. In this talk, I want to explore how to define data types describing a binary data formats and generate the corresponding serialization and deserialization functions from such descriptions. By embedding these data types in a general purpose dependently typed programming language such as Agda, we can verify once and for all that the serialization/deserialization functions generated in this style are correct by construction. To validate this approach, I will sketch how to write a verified parser for IPv4 network packets.

Bio:

Wouter Swierstra is an assistant professor at the Utrecht University in the Netherlands. After originally studying Mathematics and Computer Science, he did his PhD under supervision of Thorsten Altenkirch at the University of Nottingham's Functional Programming Lab. He worked as a postdoc at Chalmers University of Technology, before moving back to the Netherlands to work at Vector Fabrics, a high-tech startup that used functional programming to facilitate the design of embedded systems. After this brief stint in industry, he returned to academia as a postdoc in Foundations Group at the Radboud University Nijmegen and Software Technology group at Utrecht University.

abstract: In 2015, a language based fundamentally on substructural typing–Rust–hit its 1.0 release, and less than a year later it has been put into production use in a number of tech companies, including some household names. The language has started a trend, with several other mainstream languages, including C++ and Swift, in the early stages of incorporating ideas about ownership. How did this come about?

Rust’s core focus is safe systems programming. It does not require a runtime system or garbage collector, but guarantees memory safety. It does not stipulate any particular style of concurrent programming, but instead provides the tools needed to guarantee data race freedom even when doing low-level shared-state concurrency. It allows you to build up high-level abstractions without paying a tax; its compilation model ensures that the abstractions boil away.

These benefits derive from two core aspects of Rust: its ownership system (based on substructural typing) and its trait system (a descendant of Haskell’s typeclasses). The talk will cover these two pillars of Rust design, with particular attention to the key innovations that make the language usable at scale. It will highlight the implications for concurrency, where Rust provides a unique perspective. It will close out with a discussion of Rust’s development process and design considerations around language and library evolution.

bio: Aaron Turon is Research Engineering Manager for the Rust team at Mozilla. He received his PhD from Northeastern University, where he studied programming language design, program verification, and low-level concurrency. His dissertation was awarded the SIGPLAN John C. Reynolds Doctoral Dissertation Award in 2014. After his PhD studies, he continued his research in concurrency verification and programming techniques as a postdoc at MPI-SWS. He joined Mozilla in 2014, and has played an active role in Rust’s development since then.

abstract:

Project E3DB is a tool for programmers who want to build an end-to-end encrypted database with sharing into their projects. We are providing a command-line client for you to play with and a Java SDK to prototype with. Over the next few weeks, we’ll be getting feedback from you, adding features, and making it ready for production.

In this talk, Isaac will discuss what E3DB is, where it’s going, and provide a tutorial for trying it out. Bring your laptop to try!

More on E3DB: https://tozny.com/blog/announcing-project-e3db-the-end-to-end-encrypted-database/

Tozny is a Galois product spin-off. Our mission is to make strong crypto easy for both developers and end users.

bio:

Isaac is a security researcher at Galois where he has lead authentication and collaboration projects for the DoD and IC. Isaac earned his master’s degree in Cybersecurity from the University of Maryland, University College, and his B.S. in Computer Science from Ohio State University. In 2013, Isaac founded Tozny, a Galois spin-off company aimed at solving the password conundrum. Easier and more secure than passwords, Tozny replaces passwords with an easy-to-use cryptographic key on a user’s mobile phone.

Data Privacy PDX will be presenting on Privacy-by-Design, the movement to integrate privacy into the original design of a product or system. This impacts product development, business planning, and legal, making it a crucial concept to understand for everyone who is concerned with data privacy. Come learn about Privacy-by-Design and how it can impact your projects.

Snacks and drinks will be provided. Hosted by Tozny.

This is the first meeting of the Data Privacy PDX meetup. In this first meeting we will do a presentation called "Encryption Pitfalls for Developers" and will spend time helping attendees set up encrypted email for their email accounts. Snacks and drinks provided. Hosted by Tozny.

abstract:

Security-critical applications constantly face threats from exploits in lower computing layers such as the OS and Hypervisor, or even attacks from malicious administrators. To protect sensitive data from such privileged adversaries, there is increasing development of secure hardware primitives, such as Intel SGX. Intel SGX instructions enable user mode applications to package trusted code and data into regions that are isolated from all other software on the machine, and also provide cryptographic primitives such as remote attestation. Our research is developing a principled approach to building cloud services with end-to-end security guarantees, including only these trusted hardware primitives in our trusted computing base. In this talk, I will demonstrate how one can use compiler and verification techniques to develop formally verified SGX programs, and demonstrate applications where Map-Reduce programs running on SGX can be certified to not leak secrets.

bio:

Rohit Sinha is currently pursuing a Ph.D. in EECS at UC Berkeley, where he works with Prof. Sanjit Seshia. His research interests include programming languages, software verification, and security.

abstract:

The domain of Internet of Things (IoT) is rapidly expanding beyond research and becoming a major industrial market with such stakeholders as major manufacturers of chips and connected objects, and fast-growing operators of low-power wide-area networks. Importantly, this emerging domain is driven by applications that leverage the infrastructure to provide users with innovative, high-value services. Because of this application-centric approach, software development plays a key role to realize the full potential of IoT.

In this talk, we argue that there is a continuum between orchestrating connected objects in the small and in the large, fostering a unified approach to application development. We examine the requirements for orchestrating connected objects and address them with domain-specific design concepts. We then show how to map these design concepts into dedicated programming patterns and runtime mechanisms.

Our work revolves around domain-specific notations integrated into a tool-based design methodology, dedicated to develop IoT applications. We have applied our work across a spectrum of infrastructure sizes; we present examples, ranging from an automated pilot in avionics, to an assisted living platform for the home of seniors, to a parking management system in a smart city.

bio:

Charles Consel is a professor of Computer Science at Bordeaux Institute of Technology. He served on the faculty of Yale University, Oregon Graduate Institute and the University of Rennes.

His research contributions cover programming languages, software engineering, operating systems, pervasive computing, and assistive computing.

He leads the Phoenix group at Inria that conducts multi-disciplinary research to design, develop, deploy and assess assistive computing support. This research combines (1) Cognitive Science to study user needs and make a rigorous assessment of assistive services; (2) Sensing and actuating expertise to support the user, based on accurate and rich interactions with the environment; (3) Computer Science to support and guide the development process of the assistive services.

abstract:

Existing modeled and verified operating systems (OS’s) typically run on uniprocessor platforms and run with interrupts mostly disabled. This makes formal reasoning more tractable: execution is mostly sequential. The eChronos OS is a real-time OS used in tightly constrained devices, running on (uniprocessor) embedded micro-controllers. It is used in the DARPA-funded HACMS program, where it runs the flight control software of a high-assurance quadcopter. To provide low latency, the eChronos OS runs with interrupts enabled and provides a preemptive scheduler. In terms of verification, this means that concurrency reasoning is required, which significantly increases the complexity: application and OS instructions may be interleaved with interrupt handler instructions.

In our work we explicitly model the effect of interrupts and their handling by the hardware and OS. We provide a general formal model of the interleaving between OS code, application code and interrupt handlers. We then instantiate this model to formalise the scheduling behavior of the eChronos OS, and prove the main scheduler property: the running task is always the highest-priority runnable task.

bio:

June Andronick is a Senior Researcher at Data61|CSIRO (formerly NICTA). Her research focuses on increasing the reliability of critical software systems, by mathematically proving that the code behaves as expected and satisfies security and safety requirements. She contributed to the seL4 correctness proof and now focuses on concurrency reasoning for OS code. She leads the concurrency software verification research in Data61, and is deputy leader of the Trustworthy Systems group. She was recognised in 2011 by MIT’s Technology Review as one of the world’s top young innovators (TR35). She holds a PhD in Computer Science from the University of Paris-Sud, France.

abstract:

Due to the exponential growth of our ability to collect, centralize, and share data in recent years we have been able tackle problems previously assumed to be insurmountable. Ubiquitous sensors, fast and efficient machine learning, and affordable commercial-off-the-shelf technologies have not only deepened our understanding of our world, but also democratized these capabilities. As a direct result of this shift, we are facing a rapidly evolving host of challenges centered around our new data-driven world. In this talk we will discuss efforts from the Trustworthy Data Engineering Laboratory (TRUST Lab) in conjunction with our partners at the World Bank, the Federal Bureau of Investigation (FBI), the Environmental Protection Agency (EPA), and the City of Cincinnati to identify and solve problems in Adversarial Machine Learning and Data Science. We will examine real case studies in debarrment and corruption in international procurement with the World Bank, cases of violations of the Resource Conservation and Recovery Act with the EPA, and human rights abuses of low income citizens by corporate slum-lords in the city of Cincinnati. In each of these cases we will show how malicious actors manipulated the data collection and data analytics process either through misinformation, abuse of regional corporate legal structures, collusion with state actors, or knowledge of underlying predictive analytics algorithms to damage the integrity of data used by machine learning and predictive analytic processes, or the outcomes derived from these processes, to avoid regulatory oversite, sanctions, and investigations launched by national and multi-national authorities. This new type of attack is growing increasingly common, and we will motivate and encourage increased research on counter measures and safe guards in information systems.

Additionally we will discuss our efforts to combat problems in data privacy and availability in modern systems, highlighting the tradeoffs involved between data availability and privacy, and introduce a new formal logic for privacy preserving data operations, and demonstrate their performability and correctness, along with metrics for their improved privacy and suitability for high-assurance areas of data science.

bio:

Dr. Eric Rozier is an Assistant Professor of Electrical Engineering and Computing Systems and head of the Trustworthy Data Engineering Laboratory at the University of Cincinnati in Cincinnati, Ohio. He has previously been named a Frontier’s of Engineering Education Faculty member by the National Academy of Engineering, a two time Eric and Wendy Schmidt Data Science for Social Good Faculty Fellow at the University of Chicago, and an IBM Research Fellow. Dr. Rozier’s research interests revolve around the intersection of Data Science and Engineering with Cybersecurity, Reliability, and Performability Engineering, with a focus on dependable computing for critial infrastructures. His work in Adversarial Machine Learning was recently featured as one of the inaugural talks for the USENIX Engima conference on emerging threats and novel attacks. Before joining the University of Cincinnati, Dr. Rozier was the founding director of the Fortinet Cybersecurity Laboratory at the University of Miami where he worked to develop and commercialize new technologies in homomorphic encryption for cloud-based systems. He earned his Ph.D. from the University of Illinois at Urbana-Champaign where he worked on applications in fault-tolerance and security with the National Center for Supercomputing Applications, and the Information Trust Institute.

abstract:

We are at the dawn of a new age in air traffic control. The airspace is full in the sense that demand for flights exceeds our capacity to add new air traffic. The time-tested current method of air traffic control has hit its scalability limit and must be replaced with a new system that is more scalable while also proving at least as safe. Now that we have the chance to redefine air traffic control from scratch, the question arises: how do we do it safely?

We explore new frontiers in symbolic model checking to scalably answer the functional allocation question: instead of analyzing one design, or comparing a pair of designs, we now need to take into account a large number of permutations and combinations of functions that comprise a large set of possible designs. We introduce a compositional, modular, parameterized approach to model generation. We comparatively analyze the design space with regard to safety on multiple levels, considering the set of possible system designs both in nominal conditions and in the presence of faults. Our analysis helps NASA narrow the possible design space, saving time and cost of later-phase evaluations, identifying both novel and known problematic design configurations. Our methods pave the way for the complexities demanded by future analysis, as the question of how to reason about adding Unmanned Aerial Systems into the national air traffic management system looms on the horizon.

bio:

NSF CAREER Award winner and recipient of the Inaugural Initiative-Inspiration-Impact Award from Women in Aerospace, Kristin Yvonne Rozier joined the faculty of the Aerospace Engineering and Computer Science Departments in Spring, 2015. Previous to that, she spent 14 years as a Research Scientist at NASA, holding civil service positions at NASA Ames Research Center (2008-2014) and NASA Langley Research Center (2001-2008).

Rozier earned her PhD in Computer Science from Rice University and MS and BS degrees from the College of William and Mary. During her tenure at NASA, she contributed research to the Aeroacoustics, and Safety-Critial Avionics groups at NASA Langley and to the Robust Software Engineering, and Discovery and Systems Health groups in the Intelligent Systems Division at NASA Ames. She has served on the NASA Formal Methods Symposium Steering Committee since working to found that conference in 2008.

Most recently, Rozier was a primary contributing researcher to the Next Generation Air Transportation System (NextGen) Air Traffic Management project of the Airspace Systems Program at NASA. She also served as Principal Investigator of an ARMD Seedling project advancing System and Safety Health Management for Unmanned Aerial Systems (UAS). Rozier is an Associate Fellow of AIAA and a Senior Member of IEEE and SWE.

abstract:

Animal movement is driven by responses to both social and non-social factors of the environment. Research across species shows that animals do not make decisions based solely on present information, e.g., at time t, but on an integrated assessment of information over recent time, e.g., t-1, t-2, etc. This raises the conundrum of how to relate distributions of animals (or humans) to conditions of the environment since prior individual experiences, possibly to unobserved conditions, contribute to the behaviors observed. I use a rich animal and environmental data set to harness and integrate the broad spectrum of behavioral research and construct a theoretical platform for describing the observed distributions of species populations. My work in the aquatic, terrestrial, and aerial environments falls into two categories, (i) better managing civil infrastructure that impacts animal movement and (ii) developing/evaluating computational abstractions of environmental sensing and individual decision-making to inform the engineering design of distributed systems in unbounded, open field environments. In the aquatic realm, I’ll share research suggesting that water acceleration “shapes” the individual movement trajectories of juvenile salmon near hydropower dams. Then, I’ll discuss how I am building off this research to understand Sonoran Pronghorn that can interfere with military training activities in the Arizona desert. Lastly, I’ll discuss bird flocking as a biological network that can inform the design of fast, light, mobile, compact, and collapsible systems (e.g., geospatial sensors) that are resilient to attack and can quickly hide.

bio:

R. Andrew Goodwin, PhD LinkedIn: http://www.linkedin.com/in/r-andrew-goodwin-a7524491

abstract:

The last decade has seen many success stories for verified programming with dependent types, including the CompCert verified C compiler, verified libraries for concurrency and security, and machine-checked proofs of results like the four color theorem and the Feit-Thompson theorem. Despite these successes, dependently typed languages are rarely used for day-to-day programming tasks. In this talk, I’ll describe several limitations of modern dependently-typed languages that are holding them back from wider adoption for practical programming. I’ll explain the historical and mathematical reasons for these limitations, and describe how we attempted to relax them in the design of the Zombie research language.

bio:

Chris Casinghino is a Senior Member of the Technical Staff at Draper Laboratory, where he develops static analysis tools in Haskell. In 2014, he completed a PhD in the programming languages group at The University of Pennsylvania. His doctoral research focused on dependently typed programming languages, exploring both their semantics and how to use them to write better programs.

Welcome to Portland Haskell Office Hours! Bring your projects, or just your excitement for learning.

We will still be taking feedback on the format of the meetup, the scheduling, and anything else that will help make this a valuable resource for you. If you are not able to attend, let us know if there's anything we can do to help make it work in the future.

As before, the front door of the building will lock at 6pm; if you get locked out, contact us via Meetup, and we'll let you in.

--

About Haskell Office Hours:

Show up with a project you'd like to share or a problem that you're stuck on, and we'll learn together in small, supportive groups! An "Office Hours" meetup is an opportunity for people of all skill levels to come together, learn, and have fun. Our goal is to focus on inclusion and active participation through teaching and mentorship.

The meetup is hosted at Galois, which uses Haskell extensively in industry, and is well-attended by Galwegians who are eager to share their excitement for Haskell and functional programming. This group is very new, so you still have an opportunity to shape how we do things. If the schedule doesn't work for you, or if we can do anything to help you feel more safe and welcome, let us know!

Welcome to Portland Haskell Office Hours! Bring your projects, or just your excitement for learning.

We will still be taking feedback on the format of the meetup, the scheduling, and anything else that will help make this a valuable resource for you. If you are not able to attend, let us know if there's anything we can do to help make it work in the future.

As before, the front door of the building will lock at 6pm; if you get locked out, contact us via Meetup, and we'll let you in.

--

About Haskell Office Hours:

Show up with a project you'd like to share or a problem that you're stuck on, and we'll learn together in small, supportive groups! An "Office Hours" meetup is an opportunity for people of all skill levels to come together, learn, and have fun. Our goal is to focus on inclusion and active participation through teaching and mentorship.

The meetup is hosted at Galois, which uses Haskell extensively in industry, and is well-attended by Galwegians who are eager to share their excitement for Haskell and functional programming. This group is very new, so you still have an opportunity to shape how we do things. If the schedule doesn't work for you, or if we can do anything to help you feel more safe and welcome, let us know!

Welcome to Portland Haskell Office Hours! Bring your projects, or just your excitement for learning.

We will be testing this new scheduling arrangement: this meeting will be on the 13th, the second Thursday of August.

We will still be taking feedback on the format of the meetup, the scheduling, and anything else that will help make this a valuable resource for you. If you are not able to attend, let us know if there's anything we can do to help make it work in the future.

As before, the front door of the building will lock at 6pm; if you get locked out, contact us via Meetup, and we'll let you in.

-- 

About Haskell Office Hours:

Show up with a project you'd like to share or a problem that you're stuck on, and we'll learn together in small, supportive groups! An "Office Hours" meetup is an opportunity for people of all skill levels to come together, learn, and have fun. Our goal is to focus on inclusion and active participation through teaching and mentorship. The meetup is hosted at Galois, which uses Haskell extensively in industry, and is well-attended by Galwegians who are eager to share their excitement for Haskell and functional programming. This group is very new, so you still have an opportunity to shape how we do things. If the schedule doesn't work for you, or if we can do anything to help you feel more safe and welcome, let us know!

abstract:

Software-dependent critical systems that impact daily life are rapidly increasing in number, size, and complexity. Unfortunately, inadequate software and systems engineering can lead to accidents that cause economic disaster, injuries, or even death. There is a growing reliance on development and verification tools to reduce costs, better manage complexity, and to increase confidence in these systems. Recent standards for critical systems have an increased emphasis on characterizing the requirements of tools used in the certification context and the particular certification obligations that these tools can discharge. In the case of avionics, DO-333 explicitly addresses the role/use of formal methods tools, e.g., allowing formal verification of code compliance to procedure contracts to complement unit testing, and DO-330 addresses tool qualifications.

In this talk, I will present the Kiasan symbolic execution framework that can be used to automatically check varying degrees of functional correctness properties of critical systems — ranging from absence of runtime errors to compositional reasoning of deep semantical contracts of complex data structures. One notable feature of Kiasan is the focus on explicating its analysis results to describe inconclusive analysis results in cases where it cannot clearly refute or verify properties. Similar to other symbolic execution tools, Kiasan generates counter-examples or test cases as evidence for (conclusive) contract violations. In contrast to others, however, Kiasan can generate strong evidence for its (conclusive) verification results in the form of Coq proof objects. This is achieved by first formalizing Kiasan’s symbolic execution (abstract) semantics in Coq and proving that it is sound and relatively complete with respect to the (concrete) semantics of the system programming language; this is done once and for all (for a particular system programming language) and establishes a relatively small trust base. We believe that Kiasan’s evidence-based trust approach can be used to help in software certifications of safety-critical systems as well as in tool qualification processes.

bio:

Robby is a Professor in the Computing and Information Sciences (CIS) Department at Kansas State University. In addition to symbolic execution-based verification, he works on dataflow framework for analyzing security vulnerability in mobile apps, device modeling for interoperable medical devices, and a hazard analysis platform. In the past, he worked on software model checking, data/predicate abstractions, program dependences (slicing), and software specification techniques.

abstract:

Modern verification techniques are becoming ever-more powerful and sophisticated, and building tools to implement them is a time-consuming and difficult task. Writing a new verifier to validate each on-paper approach is impractical; for this reason intermediate verification languages such as Boogie and Why3 have become popular over the last decade for implementing research from a wide variety of domains, and several mature tools used in industry have been built around this common tool stack.

Reasoning approaches which orient around sophisticated partitioning and organisation of the verification state (such as separation logics) have typically been implemented in specialised tools, since the reasoning is hard to map down to first-order automated reasoning. In practice (with notable exceptions), this means that a rich variety of modern techniques have no corresponding tool support.

In this talk, I will present the new Silver intermediate verification language, which has been designed to facilitate the lightweight implementation of a variety of modern methodologies for program verification. In contrast to lower-level verification languages, Silver provides native support for heap reasoning; modes of reasoning such as concurrent separation logic, dynamic frames and rely-guarantee/invariants can be simply encoded.

Silver has been developed as part of the Viper project, which provides two automated back-end verifiers for Silver programs. Since releasing our software in September last year, it has been used for (internal and external) projects to build tools for Java verification, non-blocking concurrency reasoning, flow-sensitive typing and reasoning about GPU and Linux kernel code.

bio:

Alex Summers obtained his PhD from Imperial College London in 2009, in the area of type systems and classical logics. Since 2008, he has worked in a variety of areas concerning software correctness and verification, at Imperial College London and ETH Zurich. His research interests include developing specification techniques for different (usually concurrent) programming paradigms, and implementing these in automatic verification tools. He was recently awarded the 2015 AITO Dahl-Nygaard Junior Prize for his work on type systems and the verification of object-oriented programs.

abstract:

Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested and subject to priorities. Interrupts can arrive at arbitrary times, leading to an explosion in the number of cases to be considered. We present a new formal approach to verifying interrupt-driven software based on symbolic execution. The approach leverages recent advances in the encoding of the execution traces of interacting, concurrent threads. We assess the performance of our method on benchmarks drawn from embedded systems code and device drivers, and experimentally compare it to conventional formal approaches that use source-to-source transformations.Our experimental results show that our method significantly outperforms conventional techniques. To the best of our knowledge, our technique is the first to demonstrate effective formal verification of low-level embedded software with nested interrupts.

bio:

Lihao Liang is a PhD student in the Department of Computer Science of University of Oxford, working with Daniel Kroening, Tom Melham and Luke Ong. His research is supported by an Intel funded project Effective Validation of Firmware. He is interested in automated software analysis and verification, particularly concurrent software and synchronization primitives such as read-copy update (RCU).

abstract:

Since the ideas were first published in 1981, verifiable election technologies have undergone decades of research successes and deployment failures. This talk will trace the history of these technologies, their evolution, and the practical challenges that they have faced. We’ll then look forward at the potential for near-term successes and the public benefits that may be derived.

bio:

Josh Benaloh is Senior Cryptographer at Microsoft Research where his research focuses on multi-party protocols. He earned his bachelor’s degree from M.I.T. and his doctorate from Yale University where his 1987 dissertation “Verifiable Secret-Ballot Elections” introduced the first application of homomorphic encryption. Dr. Benaloh serves as a director of the 1500-member International Association for Cryptologic Research and chairs the Citizen Oversight Panel for Sound Transit which is investing nearly $1 billion annually on improvements to the Seattle-area transit infrastructure.

abstract:

Why is cybersecurity such a hard problem? The US government, its citizens, and the organizations that write software are all on the same team, but in many cases, our interests are just not aligned. For instance, there have been endless political and social disagreements about the best way to share cyber threat intelligence without sacrificing consumer privacy.

It’s these competing concerns that are the kink in our collective armor and that’s what our adversaries exploit, day-in and day-out.

In this talk, Isaac will present the high-level strategic concerns and challenges in the cybersecurity industry, how those challenges interact with emerging policy and law, and how those policies will impact you.

bio:

Isaac is a security researcher at Galois where he has lead authentication and collaboration projects for the DoD and IC. Isaac earned his master’s degree in Cybersecurity from the University of Maryland, University College, and his B.S. in Computer Science from Ohio State University. In 2013, Isaac founded Tozny, a Galois spin-off company aimed at solving the password conundrum. Easier and more secure than passwords, Tozny replaces passwords with an easy-to-use cryptographic key on a user’s mobile phone.

abstract: Portland State Aerospace Society (PSAS) is a student aerospace engineering project at Portland State University. We’re building ultra-low-cost, open source rockets that feature some of the most sophisticated amateur rocket avionics systems anywhere. Learn some of the history of the group, why steering a rocket is very, very hard, what we’re doing to solve that problem.

bio: Open-Source Rocket Scientist. Currently the program manager of the Lab for Interconnected Devices at Portland State University — an electronics rapid prototyping playground for engineering students. Nathan has spent the last 7 years helping build a homegrown space program at PSU through volunteering at the Portland State Aerospace Society (PSAS).

abstract: For the last several years, speed improvements in computing come mainly from increasing parallelism. Imperative programming, however, makes parallelization very difficult due to the many possible dependencies implied by effects. For decades, pure functional programming has held the promise of parallel execution while retaining the very simple semantics that enables practical, rigorous reasoning. This talk describes a prototype compiler from Haskell (not a library) to low-level hardware descriptions for massively parallel execution on reprogrammable logic devices. The compiler works by monomorphizing, miscellaneous other transformations, and conversion to the vocabulary of cartesian closed categories (CCCs), as captured in a small collection of Haskell type classes. One instance of those classes provides an interpretation as parallel circuits. I will show many examples of simple Haskell programs and corresponding compiler-generated circuits.

bio: Conal Elliott has been working (and playing) in functional programming for more than 30 years. He especially enjoys applying semantic elegance and rigor to library design and optimized implementation. He invented the paradigm now known as “functional reactive programming” in the early 1990s, and then pioneered compilation techniques for high-performance, high-level embedded domain-specific languages, with applications including 2D and 3D computer graphics. The latter work included the first compilation of Haskell programs to GPU code, while maintaining precise and simple semantics and powerful composability, as well a high degree of optimization. Conal earned a BA in math with honors from the College of Creative Studies at UC Santa Barbara in 1982 and a PhD in Computer Science from Carnegie Mellon University in 1990. His latest position was at Tabula Inc, where he worked on chip specification and compiling Haskell to hardware for massively parallel execution until their closure in early 2015. Before Tabula, his positions included Architect at Sun Microsystems and Researcher in the Microsoft Research graphics group. He has also coached couples and led conscious relationship workshops together with his partner Holly Croydon, with whom he now lives on 20 acres in the woods in the California Gold Country. For publications, CV, professional blog, etc, see http://conal.net.

abstract: Jesse has been using Rust to write a PAM module. He will tell us about what he has learned about working with Rust, and about getting Rust’s lifetime-checking to mesh with external C functions.

bio: Jesse Hallett is a research engineer at Galois. He has extensive experience in web and high-level programming; but has only recently ventured into system programming. It has been said that Rust makes system programming accessible to people who wouldn’t touch C++ with a 12-foot pole. Jesse is one of those people. And he is interested in talking about how Rust helps him to access a wider world of programming.

abstract: Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as well as using its development tools. Topics to be covered include the basics of dependent types, embedding DSLs in Idris, Idris’s notion of type providers, a general outline of the implementation strategy, the C FFI, and the effects library. Each talk has an associated set of exercises as well as suggested projects for further learning. Participants are expected to be familiar with functional programming in either Haskell or an ML.

bio: David Raymond Christiansen is a Ph.D. student at the IT University of Copenhagen. For the last few months, he has been an intern at Galois, working on verifiable elections and better user interfaces for DSLs. His interests include functional programming languages, domain-specific languages, and environments that make them useful. David has contributed features such as type providers and error reflection to the Idris language as well as significant parts of the Emacs-based IDE. Additionally, he is a co-host of The Type Theory Podcast.

abstract: Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as well as using its development tools. Topics to be covered include the basics of dependent types, embedding DSLs in Idris, Idris’s notion of type providers, a general outline of the implementation strategy, the C FFI, and the effects library. Each talk has an associated set of exercises as well as suggested projects for further learning. Participants are expected to be familiar with functional programming in either Haskell or an ML.

bio: David Raymond Christiansen is a Ph.D. student at the IT University of Copenhagen. For the last few months, he has been an intern at Galois, working on verifiable elections and better user interfaces for DSLs. His interests include functional programming languages, domain-specific languages, and environments that make them useful. David has contributed features such as type providers and error reflection to the Idris language as well as significant parts of the Emacs-based IDE. Additionally, he is a co-host of The Type Theory Podcast.

abstract: Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as well as using its development tools. Topics to be covered include the basics of dependent types, embedding DSLs in Idris, Idris’s notion of type providers, a general outline of the implementation strategy, the C FFI, and the effects library. Each talk has an associated set of exercises as well as suggested projects for further learning. Participants are expected to be familiar with functional programming in either Haskell or an ML.

bio: David Raymond Christiansen is a Ph.D. student at the IT University of Copenhagen. For the last few months, he has been an intern at Galois, working on verifiable elections and better user interfaces for DSLs. His interests include functional programming languages, domain-specific languages, and environments that make them useful. David has contributed features such as type providers and error reflection to the Idris language as well as significant parts of the Emacs-based IDE. Additionally, he is a co-host of The Type Theory Podcast.

bio: Evan Wright is a member of the Technical Staff for the Threat Discovery Group of the CERT Coordination Center (CERT/CC). The CERT/CC is a division of the Software Engineering Institute at Carnegie Mellon University. He holds a MS in Information Security and Technology Management from Carnegie Mellon University and a BS in Technology Systems from East Carolina University. He has over 20 years experience in computer networking and holds a CCNP and six other certifications. Since joining SEI, he has supported a variety of customers in areas such as IPv6 security, ultra-large scale network monitoring, malicious network traffic detection, intelligence fusion, and cybersecurity applications of machine learning. Before joining SEI, he was a network administrator for a medium sized company and Internet Service Provider in North Carolina.

abstract: If you do a web search for “encrypting Strings in Android”, you’ll find a lot of example code, and they all look pretty similar. They definitely input a String and output gibberish that looks like encrypted text, but they are often incorrect. Crypto is tricky: it’s hard to tell that the gibberish that’s being printed is not good crypto, and it’s hard to tell that the code example you picked up from Stack Overflow has serious flaws.

The problem here is that sites like Google and Stack Overflow rank results based on popularity, but the correctness of crypto isn’t something we can vote about. It’s not a popularity contest. To use it correctly, you have to understand the properties of the algorithm and the security goals of your code. Maybe the bad crypto someone pasted up on the Internet was acceptable for their needs, but there’s a good chance it’s completely unacceptable for yours.

In this talk, we’ll discuss the use of a very common crypto algorithm, AES, and show how code examples on the Internet usually make serious mistakes in how they use AES libraries. What are the consequences of these mistakes and what are more reasonable defaults. We’ll also talk a bit about our simple Android library that tries to do AES right.

More information on the Tozny blog: http://tozny.com/blog/encrypting-strings-in-android-lets-make-better-mistakes/

bio: Isaac is a security researcher at Galois where he has lead authentication and collaboration projects for the DoD and IC. Isaac earned his master’s degree in Cybersecurity from the University of Maryland, University College, and his B.S. in Computer Science from Ohio State University. In 2013, Isaac founded Tozny, a Galois spin-off company aimed at solving the password conundrum. Easier and more secure than passwords, Tozny replaces passwords with an easy-to-use cryptographic key on a user’s mobile phone.

abstract: GHC is a state-of-the-art optimizing compiler that is constantly being improved. But despite all of the hard work by the developers, you occasionally find yourself in need of a feature that GHC does not (yet) support. Luckily for us, GHC does have multiple extension points built into the standard compilation pipeline, in addition to exposing its functionality as a library.

In this talk I’ll give an overview of GHC’s internal architecture and existing extension points. I’ll also walk through a recent extension I wrote to improve the debugging experience in embedded DSLs.

bio: Eric Seidel is a 3rd year PhD student at UC San Diego, where he works on the LiquidHaskell program-verification tool.

abstract: Read-copy update (RCU) is a synchronization mechanism that is sometimes used as an alternative to reader-writer locking (among other things) that was added to the Linux kernel in 2002. A similar mechanism was added to Sequent’s DYNIX/ptx parallel UNIX kernel in 1993, and antecedents go back to at least 1980. Although a fully functional textbook implementation of RCU comprises only about 20 lines of code, the Linux-kernel implementation comprises more than 15,000 lines of code due to harsh requirements involving performance, scalability, energy efficiency, real-time response, memory footprint, module unloading, hotplugging of CPUs, and software-engineering considerations.

Therefore, a key Linux-kernel RCU challenge is validation and verification. To this end, more than 2500 lines of the current Linux-kernel implementation do torture testing. However, there are now more than one billion devices running Linux, so that an RCU bug that manifested on average once every million years of machine time would manifest about three times every day across the installed base. Furthermore, the combination of Internet of Things and Josh Triplett’s Linux Kernel Tinification project is likely to significantly increase the number of running instances.

I write and run rcutorture tests myself, and I like to think that my 20 years of parallel-code testing experience allows me to meet this validation challenge, but a simple analysis suggests a gap of several orders of magnitude. Additional validation and verification techniques are thus called for. This talk gives a brief overview of RCU and describes my adventures evaluating various verification techniques.

bio: Paul E. McKenney has been coding for almost four decades, more than half of that on parallel hardware, where his work has earned him a reputation among some as a flaming heretic. Over the past decade, Paul has been an IBM Distinguished Engineer at the IBM Linux Technology Center. Paul maintains the RCU implementation within the Linux kernel, where the variety of workloads present highly entertaining performance, scalability, real-time response, and energy-efficiency challenges. Prior to that, he worked on the DYNIX/ptx kernel at Sequent, and prior to that on packet-radio and Internet protocols (but long before it was polite to mention Internet at cocktail parties), system administration, business applications, and real-time systems. He has a BS in Computer Science and another in Mechanical Engineering along with an MS in Computer Science, all from Oregon State University. He also has a Ph.D. in Computer Science and Engineering from OGI/OHSU. He has more than 100 publications and more than 50 patents. His hobbies include what passes for running at his age along with the usual house-wife-and-kids habit.

Welcome to Portland Haskell Office Hours! Bring your projects, or just your excitement for learning.

The construction in the Galois offices is finished, so we are able to resume our regular meeting location. As before, the front doors of the building lock at 6pm, so please give me a call at[masked] if you arrive late.

We will still be taking feedback on the format of the meetup, the scheduling, and anything else that will help make this a valuable resource for you. If you are not able to attend, let us know if there's anything we can do to help make it work in the future.

-- 

About Haskell Office Hours:

Show up with a project you'd like to share or a problem that you're stuck on, and we'll learn together in small, supportive groups! An "Office Hours" meetup is an opportunity for people of all skill levels to come together, learn, and have fun. Our goal is to focus on inclusion and active participation through teaching and mentorship. The meetup is hosted at Galois, which uses Haskell extensively in industry, and is well-attended by Galwegians who are eager to share their excitement for Haskell and functional programming. This group is very new, so you still have an opportunity to shape how we do things. If the schedule doesn't work for you, or if we can do anything to help you feel more safe and welcome, let us know!