Search

To detect and mitigate security vulnerabilities early in the coding phase is an important strategy for secure software development. Existing solutions typically focus on finding certain vulnerabilities in certain computer systems without giving a systematic way of handling different types of vulnerabilities. In this paper, we present a framework for systematically modeling and detecting potential security vulnerabilities during the construction of programs using a particular programming paradigm known as Human-Machine Pair Programming. The framework provides designers with a general way of modeling a class of attacks in detail, and shows how programmers can discover and fix a vulnerability in a timely manner. Specifically, our framework advocates three primary steps: (1) generating an attack tree to model a given security threat, (2) constructing vulnerability-matching patterns based on the result of the attack tree analysis, and (3) detecting corresponding vulnerabilities based on the patterns during the program construction. We also present a case study to demonstrate how it works in practice. &nbsp

International audience; We present a formal approach based on mutation techniques for the modelling of cybersecurity attacks and its application to 5G networks. We introduce formal definitions of the main concepts of network protocols, mutation operators, flow of network packets and network traffic. We design a formal approach based on different mutation operators that allows to design models that can be assimilated with known and unknown attacks. This approach has been implemented in our open source 5G network traffic fuzzer, 5Greplay, and has been applied to two use cases that are representative of attacks against 5G networks.

Software systems are more and more complex. They are usually constructed by combining several components which can be implemented separately and deployed in distributed environments. This paper presents a framework for testing these kind of systems. Particularly, each component of a system is tested by a tester and there is no communication between testers. The tester is guided by local test cases that are generated from the composition of models of components where the communication among components may be synchronous or asynchronous. The framework is complemented with a tool chain for automating test generation. The paper presents also a case study on the European Train Control System.

8 pages - Short papers session (http://ictss2011.lri.fr/); International audience; This paper addresses the problem of the choice of a coverage measure for hybrid automata. We propose a parametric measure inspired by the notion of operational profile that allows the tester to specify his testing objectives as a required, locally defined 'density' of test cases. The characteristics of our measure and the operational profiles are motivated by the testing context of Home Automation Systems. We compare this measure with related work and show that it yields improvements over several existing measures in our context.