Determinacy is a desirable but difficult-to-achieve behavioural property in scalable distributed systems. Deterministic Models of Computation range from the asynchronous Kahn Process Networks to synchronous reactive languages such as Lustre, where logical clocks enforce the synchrony hypothesis. These models have well-founded data-flow s emantics w here computations are viewed as the least fixed point solutions of simultaneous equations defined by continuous functions on streams of discrete values. However, scalable and efficient implementations of the Kahn model are challenging to construct, while the synchrony hypothesis in Lustre makes distributed implementations difficult. Moreover, determinacy is a consequence of specific assumptions built into the computational model. The notion of Logical Synchrony, proposed by Lall et al., and explored further by Kenwright et al., suggests that synchronisation issues may be decoupled from computation, leading to a distributed model where computations at independent nodes are related by invariant logical delays. We provide a semantic notion of behaviour for functional processes running on such Logical Synchrony Networks (extension graphs), and an appropriate and robust notion of logical observational equivalence (wavefront equivalence) retaining semantic aspects of KPNs, specifically determinacy. Further, we propose extending the versatile notion of the synchronous observer, exploited in the Lustre toolset, to a network of located synchronous observers with the same invariant logical delays as the distributed system. Thus we will be able to use the same logically synchronous model of computation for checking or monitoring a class of (safety) properties of programs, specifying axioms and assumptions on behaviour, constraining models and specifying test cases, etc.

Synchronous reactive data flow is a paradigm that provides a high-level abstract programming model for embedded and cyber-physical systems, including the locally synchronous components of IoT systems. Security in such systems is severely compromised due to low-level programming, ill-defined interfaces and inattention to security classification of data. By incorporating a Denning-style lattice-based secure information flow framework into a synchronous reactive data flow language, we provide a framework in which correct-and-secure-by-construction implementations for such systems can be specified and derived. In particular, we propose an extension of the Lustre programming framework with a security type system. We prove the soundness of our type system with respect to the co-inductive operational semantics of Lustre by showing that well-typed programs exhibit non-interference.

Runtime verification employs dedicated hardware or software monitors to check whether program properties hold at runtime. However, these monitors often incur high area and performance overheads depending on whether they are implemented in hardware or software. In this work, we propose DHOOM, an architectural framework for runtime monitoring of program assertions, which exploits the combination of a reconfigurable fabric present alongside a processor core with the vestigial on-chip Design-for-Debug hardware. This combination of hardware features allows DHOOM to minimize the overall performance overhead of runtime verification, even when subject to a given area constraint. We present an algorithm for dynamically selecting an effective subset of assertion monitors that can be accommodated in the available programmable fabric, while instrumenting the remaining assertions in software. We show that our proposed strategy, while respecting area constraints, reduces the performance overhead of runtime verification by up to 32% when compared with a baseline of software-only monitors.

The Internet of Things (IoT) is an extension of the traditional Internet, which allows a very large number of smart devices, such as home appliances, network cameras, sensors and controllers to connect to one another to share information and improve user experiences. IoT devices are micro-computers for domain-specific computations rather than traditional function-specific embedded devices. This opens the possibility of seeing many kinds of existing attacks, traditionally targeted at the Internet, also directed at IoT devices. As shown by recent events, such as the Mirai and Brickerbot botnets, DDoS attacks have become very common in IoT environments as these lack basic security monitoring and protection mechanisms. In this paper, we propose a novel light-weight approach for detecting DDos malware in IoT environments. We extract the malware images (i.e., a one-channel gray-scale image converted from a malware binary) and utilize a light-weight convolutional neural network for classifying their families. The experimental results show that the proposed system can achieve 94:0% accuracy for the classification of goodware and DDoS malware and 81:8% accuracy for the classification of goodware and two main malware families.

We study the problem of enforcing information flow control (IFC) in ehealth systems to verify secure flow of information through programs. IFC mechanisms allow users to control the release and propagation of sensitive information so that confidential information is not observable to unintended principals while collaborating with other legitimate principals. We formalise the parametrised security classes that are required for security policy specification in typical e-health systems in a hospital and use static type checking for detecting security policy violations in the system. The key advantage of using the parametrised security class lattice is greater precision in stating policies, enhanced usability and a reduced overhead in creating security tags.

The "one-architecture-fits-all" design philosophy is inadequate for catering to the diverse characteristics of applications running on manyCore architectures. After evaluating various configurations of manyCore architectures for a variety of applications, we designed ReKonf, a reconfigurable adaptive manyCore architecture. ReKonf dynamically configures its reconfigurable components to morph into significantly different configurations on the same architecture by continuously monitoring vital parameters of applications. ReKonf adapts the architecture by tracking core utilization, live cache utilization and cache sharing between threads, at runtime without losing execution state. Our evaluation of various applications on a cycle accurate simulator shows that the (reconfigurable) architecture suitable for such applications can be classified into three main variants: Chip Multiprocessor mode; Symmetric Multiprocessor mode; and Clustered mode, with up to 256 processing cores. Our results show that improvements from 32% to 72% over a baseline configuration can be observed by choosing the right configuration for an application. We also propose architecture components that should be reconfigurable in future manyCore architectures.

The de facto service architecture of today's communication networks, in particular the Internet, is heterogeneous, complex, ad hoc, and not particularly well understood. With layering as the only means for functional abstraction, and even this violated by middle-boxes, the diversity of current technologies can barely be expressed, let alone analyzed. As a first step to remedying this problem, we present an axiomatic formulation of fundamental forwarding mechanisms in communication networks. This formulation allows us to express precisely and abstractly the concepts of naming and addressing and to specify a consistent set of control patterns and operational primitives, from which a variety of communication services can be composed. Importantly, this framework can be used to (1) formally analyze network protocols based on structural properties, and also to (2) derive working prototype implementations of these protocols. The prototype is implemented as a universal forwarding engine, a general framework and runtime environment based on the Click router.