SRC Posters
June 4th, Wednesday, 3:30 pm - 4:30 pm
Session Chairs:Romain Robbes, Aditya Nori
Room: TBA
Exception Handling for Dynamic Information Flow Control
Abhishek Bichhawat
(Saarland University, Germany)
Exceptions are a source of information leaks, which are difficult to handle as they allow for non-local control transfer. Existing dynamic information flow control techniques either ignore unstructured control flow or are restrictive. This work presents a more permissive solution for controlling information leaks using program analysis techniques.
Automatic Performance Modeling of Multithreaded Programs
Alexander Tarvo
(Brown University, USA)
Multithreaded programs express a complex non-linear dependency between their configuration and the performance. To better understand this dependency performance prediction models are used. However, building performance models manually is time-consuming and error-prone. We present a novel methodology for automatically building performance models of industrial multithreaded programs.
Incremental Reachability Checking of KernelC Programs using Matching Logic
Alessandro Maria Rizzi
(Politecnico di Milano, Italy)
A fundamental phase in software development deals with verifying that software behaves correctly. Although accurate testing can discover many wrong behaviours, formal software verification techniques can help in developing applications that dependably satisfy their requirements. However, since formal verification techniques are time consuming and software changes continuously, incremental verification methods, i.e., methods which reuse the results of the verification of a previous version when verifying a new version of a program, are very useful, since they can significantly reduce the time required to perform the verification. In this work I apply a syntactic-semantic incremental approach to reachability checking of KernelC programs using matching logic. KernelC is a significant, non-trivial subset of the C programming language. Matching logic is a language-independent proof system to reason about programs in any language that has a rewrite-based operational semantics. Incrementality is achieved by encoding the verification procedure in a syntax-driven fashion based on semantic attributes defined on top of an operator-precedence grammar.
Exploiting Undefined Behaviors for Efficient Symbolic Execution
Asankhaya Sharma
(National University of Singapore, Singapore)
Symbolic execution is an important and popular technique used in several software engineering tools for test case generation, debugging and program analysis. As such improving the performance of symbolic execution can have huge impact on the effectiveness of such tools. In this paper, we present a technique to systematically introduce undefined behaviors during compilation to speed up the subsequent symbolic execution of the program. We have implemented our technique inside LLVM and tested with an existing symbolic execution engine (Pathgrind). Preliminary results on the SIR repository benchmark are encouraging and show 48% speed up in time and 30% reduction in the number of constraints.
Identifying Caching Opportunities, Effortlessly
Alejandro Infante
(University of Chile, Chile)
Memory consumption is a great concern for most non trivial software. In this paper we introduce a dedicated code profiler that identifies opportunities to reduce memory consumption by introducing caches.
Program Transformations to Fix C Buffer Overflow
Alex Shaw
(Auburn University, USA)
This paper describes two program transformations to fix buffer overflows originating from unsafe library functions and bad pointer operations. Together, these transformations fixed all buffer overflows featured in 4,505 programs of NIST’s SAMATE reference dataset, making the changes automatically on over 2.3 million lines of C code.
Characteristics of the Vulnerable Code Changes Identified through Peer Code Review
Amiangshu Bosu
(University of Alabama, USA)
To effectively utilize the efforts of scarce security experts, this study aims to provide empirical evidence about the characteristics of security vulnerabilities. Using a three-stage, manual analysis of peer code review data from 10 popular Open Source Software (OSS) projects, this study identified 413 potentially vulnerable code changes (VCC). Some key results include: 1) the most experienced contributors authored the majority of the VCCs, 2) while less experienced authors wrote fewer VCCs, their code changes were 1.5 to 24 times more likely to be vulnerable, 3) employees of the organization sponsoring the OSS projects are more likely to write VCCs.
Privacy and Security Requirements Framework for the Internet of Things (IoT)
Israa Alqassem
(Masdar Institute of Science and Technology, United Arab Emirates)
Capturing privacy and security requirements in the very early stages is essential for creating sufficient public confidence in order to facilitate the adaption of novel systems such as the Internet of Things (IoT). However, traditional requirements engineering methods and frameworks might not be sufficiently effective when dealing with new types of IoT heterogeneous systems. Therefore, building a methodological framework to model the privacy and security requirements specifications for IoT is necessary in order to deal with its mission critical nature. The purpose of this project is to develop such a requirements engineering framework in order to ensure proper development of IoT with security and privacy taken into account from the earliest stages.