Abstract Intrusion detection has been studied extensively from different perspectives in the last three decades. In this paper, we have developed a tool called Malfor (short for MALware FORensics), which avoids some drawbacks in the existing systems by using experimental methods. The proposed system, Malfor, captures events (processes in our case) as the system is running. As soon as a break-in... Intrusion detection has been studied extensively from different perspectives in the last three decades. In this paper, we have developed a tool called Malfor (short for MALware FORensics), which avoids some drawbacks in the existing systems by using experimental methods. The proposed system, Malfor, captures events (processes in our case) as the system is running. As soon as a break-in is detected, Malfor uses these events to replay the system partially. By cleverly choosing which events to repeat, we isolate those relevant to the break-in. Thus, this system uses experimental methods to analyse intrusions automatically. It can be used on production systems and is especially suitable for the analysis of targeted attacks. Read More Read Less

Abstract Embedded systems that are self-adaptive automatically adjust to changing environmental conditions to enhance their performance and reliability by reducing functionality in the event of failure. However, the adaptive behaviour of embedded systems significantly challenges system design and presents new challenges for ensuring system correctness, especially in the automotive domain. Therefore, formal verification applied in safety-critical applications must address dynamic adaptation... Embedded systems that are self-adaptive automatically adjust to changing environmental conditions to enhance their performance and reliability by reducing functionality in the event of failure. However, the adaptive behaviour of embedded systems significantly challenges system design and presents new challenges for ensuring system correctness, especially in the automotive domain. Therefore, formal verification applied in safety-critical applications must address dynamic adaptation in terms of time and functional properties and in terms of dynamic adaptation in terms of external and internal cues. In this paper, we present a formal semantic-based framework for modelling, specifying and verifying functional and adaptation behaviour of Synchronous Adaptive Systems. Modular reasoning and abstraction mechanisms allow automatic model checking to be efficiently applied. The modelling distinguishes functional and adaptive behaviours to reduce the design complexity and allows modular reasoning on both aspects independently and in combination. An example shows how to use the framework to validate the properties of Synchronous Adaptive Systems. Read More Read Less

Abstract In this work, we introduced a scalable interface model and the tools for them, which is called TICC. The paper begins with exploring the interface theory and then introduces the social interface model, a game-based interface model with rich communication primitives to model software and distributed systems. The model and its key features are discussed in detail and illustrated with... In this work, we introduced a scalable interface model and the tools for them, which is called TICC. The paper begins with exploring the interface theory and then introduces the social interface model, a game-based interface model with rich communication primitives to model software and distributed systems. The model and its key features are discussed in detail and illustrated with the help of TICC. Read More Read Less