Biblio

Due to its ability to detect many frequently occurring security vulnerabilities, taint analysis is one of the core static analyses used by many static application security testing (SAST) tools. Previous studies have identified issues that software developers face with SAST tools. This paper reports on our experience in building a configurable taint analysis tool, named SecuCheck, that runs in multiple integrated development environments. SecuCheck is built on top of multiple existing components and comes with a Java-internal domain-specific language fluentTQL for specifying taint-flows, designed for software developers. We evaluate the applicability of SecuCheck in detecting eleven taint-style vulnerabilities in microbench programs and three real-world Java applications with known vulnerabilities. Empirically, we identify factors that impact the runtime of SecuCheck.

An effective way for building secure software is to embed security into software in the early stages of software development. Thus, we aim to study several evidences of code anomalies introduced during the software development phase, that may be indicators of security issues in software, such as code smells, structural complexity represented by diverse software metrics, the issues detected by static code analysers, and finally missing security best practices. To use such evidences for vulnerability prediction and removal, we first need to understand how they are correlated with security issues. Then, we need to discover how these imperfect raw data can be integrated to achieve a reliable, accurate and valuable decision about a portion of code. Finally, we need to construct a security actuator providing suggestions to the developers to remove or fix the detected issues from the code. All of these will lead to the construction of a framework, including security monitoring, security analyzer, and security actuator platforms, that are necessary for a security-aware integrated development environment (SIDE).

Security protocols are critical components for the construction of secure and dependable distributed applications, but their implementation is challenging and error prone. Therefore, tools for formal modelling and analysis of security protocols can be potentially very useful to support software engineers. However, despite such tools have been available for a long time, their adoption outside the research community has been very limited. In fact, most practitioners find such applications too complex and hardly usable for their daily work. In this paper, we present an Integrated Development Environment for the design, verification and implementation of security protocols, aimed at lowering the adoption barrier of formal methods tools for security. In the spirit of Model Driven Development, the environment supports the user in the specification of the model using the simple and intuitive language AnB (and its extension AnBx). Moreover, it provides a push-button solution for the formal verification of the abstract and concrete models, and for the automatic generation of Java implementation. This Eclipse-based IDE leverages on existing languages and tools for modelling and verification of security protocols, such as the AnBx Compiler and Code Generator, the model checker OFMC and the protocol verifier ProVerif.

FeatureIDE is an open-source framework to model, develop, and analyze feature-oriented software product lines. It is mainly developed in a cooperation between University of Magdeburg and Metop GmbH. Nevertheless, many other institutions contributed to it in the past decade. Goal of this tutorial is to illustrate how FeatureIDE can be used to clean variable code, whereas we will focus on dependencies in feature models and on variability implemented with preprocessors. The hands-on tutorial will be highly interactive and is devoted to practitioners facing problems with variability, lecturers teaching product lines, and researchers who want to safe resources in building product line tools.