Abstract

Abstract
Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Given such a team automaton, we can reason over communication properties such as receptiveness (sent messages must be received) and responsiveness (pending receives must be satisfied). Previous work focused on how to identify these communication properties. However, automatically verifying these properties is non-trivial, as it may involve traversing networks of interacting automata with large state spaces. This paper investigates (1) how to characterise communication properties for team automata (and subsumed models) using test-free propositional dynamic logic, and (2) how to use this characterisation to verify communication properties by model checking. A prototype tool supports the theory, using a transformation to interact with the mCRL2 tool for model checking. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Abstract

Abstract
The increasing number of IoT devices and digital services offers cross-domain sensing and control opportunities to a growing set of stakeholders. The provision of cross-domain digital services requires interoperability as a key enabler to bridge domain specifics, while inferring knowledge and allowing new data-driven services. This work addresses H2020 InterConnect project's Interoperability Framework, highlighting the use of semantic web technologies. The interoperability framework layering is presented, particularly addressing the Semantic Interoperability layer as its cornerstone to build an interoperable ecosystem of cross-domain digital services via a federation of distributed knowledge bases. Departing from a generic, ontology-agnostic approach that can fit any cross-domain use case, it validates the approach by considering the SAREF family of ontologies, showcasing an IoT and energy cross-domain use case.

Abstract

Abstract
With continuous technological advancement, multihomed devices are becoming common. They can connect simultaneously to multiple networks through different interfaces. However, since TCP sessions are bound to one interface per device, it hampers applications from taking advantage of all the available connected networks. This has been solved by MPTCP, introduced as a seamless extension to TCP, allowing more reliable sessions and enhanced throughput. However, MPTCP comes with an inherent risk, as it becomes easier to fragment attacks towards evading NIDS. This paper presents a study of how MPTCP can be used to evade NIDS through simple cross-path attacks. It also introduces tools to facilitate assessing MPTCP-based services in diverse network topologies using an emulation environment. Finally, a new solution is proposed to prevent cross-path attacks through uncoordinated networks. This solution consists of a hostlevel plugin that allows MPTCP sessions only through trusted networks, even in the presence of a NAT.