Abstract: Combinatorial methods have attracted attention as a means of providing strong assurance at reduced cost, but when are these methods practical and cost-effective? This tutorial comprises of two parts. The first introductory part will briefly explain the background, process, and tools available for combinatorial testing, with illustrations from industry experience with the method.
The main part, explains combinatorial testing-based techniques for effective security testing of software components and large-scale software systems. It will develop quality assurance and effective re-verification for security testing of web applications and security testing of operating systems. It will further address how combinatorial testing can be applied to ensure proper error-handling of network security protocols and provide the theoretical guarantees for exciting Trojans injected in cryptographic hardware. Procedures and techniques, as well as workaround will be presented and captured as guidelines for a broader audience. The tutorial is concluded with our vision for combinatorial security testing together with some current open research problems.

Bio: Dr. Dimitris E. Simos is a Key Researcher with SBA Research, Austria, for the “applied discrete mathematics for information security” research area where he is leading the combinatorial security testing team. He is also an Adjunct Lecturer with Vienna University of Technology and a Distinguished Guest Lecturer with Graz University of Technology.
His research interests include the application of combinatorial designs to software testing, combinatorial testing in particular, error-correcting codes and their applications to post-quantum cryptography, optimization algorithms for discrete structures, symbolic computation and in general all mathematical aspects of information security.
He holds a Ph.D. in Discrete Mathematics and Combinatorics (2011) from the National Technical University of Athens. Prior to joining SBA Research, he was within the Project Team SECRET of INRIA Paris-Rocquencourt Research Center working on the design and analysis of cryptographic algorithms. His research was supported by a 3-year Marie Curie Fellow grant (2012-2015) awarded by the ERCIM through the EU-funded “Alain Bensoussan” Fellowship Programme. He is also a Fellow of the Institute of Combinatorics and its Applications (FTICA) since 2012.

Abstract: Machine Learning projects have already shown significant value in variety of areas, including design and validation fields. However, in practice, the process of bringing a valuable ML project into production can come across many hurdles, thus It is extremely difficult to truly embed them in the core processes of the organization.
In this tutorial we will present some best practices in working on ML projects, deploying them in core processes, and maximizing the value they create. We will focus on CRISP-DM methodology, Agile ML development process and others topics, as well as present some examples from projects conducted for Intel’s validation teams.

Bio: Data Scientist Leader at Intel’s Advanced Analytics group, which provides solutions to many business units in Intel. Litan’s team is focusing on ML and Big Data solutions for the design & Validation teams in intel.
Litan owns a M.Sc. degree in Information-Systems Engineering at BGU (focused on Machine-Learning and Reinforcement-Learning)

Abstract: Software Model Checking (SMC) is one of the most effective automated program verification techniques available today. SMC is applicable to a large range of programs and properties and is capable of producing both counterexamples (i.e., program executions that show how the property is violated by the program) and certificates (i.e., inductive proofs that justify how the property is satisfied in all program executions). In this tutorial, I will demonstrate a Software Model Checker SeaHorn, currently developed in a collaboration between University of Waterloo and SRI International. SeaHorn provides a verification environment build on top of LLVM -- an industrial compiler infrastructure. SeaHorn combines traditional and advanced Software Model Checking algorithms based on Satisfiability Modulo Theory (SMT) with Abstract Interpretation and many unique abstract domains. While being state-of-the-art SMC, SeaHorn provides infrastructure for conducting research in automated program analysis.

Bio: Prof. Arie Gurfinkel holds a Ph.D. in Computer Science from the Computer Science Department of University of Toronto (2007). He is an Associate Professor at the Department of Electrical and Computer Engineering at the University of Waterloo. Between 2007 and 2016, he was a Principal Researcher at the Carnegie Mellon Software Engineering Institute. His research interests lie in the intersection of formal methods and software engineering, with an emphasis on automated reasoning about software systems. He has co-lead development of a number of automated verification tools including the first multi-valued model-checker XChek, award winning software verification frameworks UFO and SeaHorn, and a hardware model-checker Avy.