Search

Proofs in simulation-based frameworks have the greatest rigor when they are machine checked. But the level of details in these proofs surpasses what the formal-methods community can handle with existing tools. Existing formal results consider streamlined versions of simulation-based frameworks to cope with this complexity. Hence, a central question is how to abstract details from composability results and enable their formal verification.In this paper, we focus on the modeling of system communication in composable security statements. Existing formal models consider fixed communication patterns to reduce the complexity of their proofs. However, as we will show, this can affect the reusability of security statements. We propose an abstract approach to modeling system communication in Constructive Cryptography that avoids this problem. Our approach is suitable for mechanized verification and we use CryptHOL, a framework for developing mechanized cryptography proofs, to implement it in the Isabelle/HOL theorem prover. As a case study, we formalize the construction of a secure channel using Diffie-Hellman key exchange and a one-time-pad.

The concepts of information flow security and refinement are known to have had a troubled relationship ever since the seminal work of McLean. In this work we study refinements that support changes in data representation and semantics, including the addition of state variables that may induce new observational power or side channels. We propose a new epistemic approach to ignorance-preserving refinement where an abstract model is used as a specification of a system’s permitted information flows, that may include the declassification of secret information. The core idea is to require that refinement steps must not induce observer knowledge that is not already available in the abstract model. Our study is set in the context of a class of shared variable multiagent models similar to interpreted systems in epistemic logic. We demonstrate the expressiveness of our framework through a series of small examples and compare our approach to existing, stricter notions of information-flow secure refinement based on bisimulations and noninterference preservation. Interestingly, noninterference preservation is not supported “out of the box” in our setting, because refinement steps may introduce new secrets that are independent of secrets already present at abstract level. To support verification, we first introduce a “cube-shaped” unwinding condition related to conditions recently studied in the context of value-dependent noninterference, kernel verification, and secure compilation. A fundamental problem with ignorance-preserving refinement, caused by the support for general data and observation refinement, is that sequential composability is lost. We propose a solution based on relational pre-and postconditions and illustrate its use together with unwinding on the oblivious RAM construction of Chung and Pass.

We introduce notions of Galois biconnections, intended to be the bilattice analogue of classical Galois connections between lattices. A bidirectional Galois biconnection is a (compatible) pair of Galois connections, the first relating truth orderings and the second relating knowledge orderings, while a unidirectional Galois biconnection is a Galois connection equipped with extra properties that seek to capture the bilattice structure. A further distinction is made between strong Galois biconnections which furnish bilattice-isomorphic images and regular Galois biconnections which induce order-isomorphic images of the maps. We investigate all four species of Galois biconnections on pre-bilattices and on bilattices with negation and conflation. We examine both the survival of elegant properties of Galois connections (composability, invertibility, preservation of joins and meets, etc.) and the preservation of interesting bilattice properties (distributivity, boundedness, interlacing) for the images of the bilattices under the Galois biconnection. Finally, we discuss the naturally emerging biclosure operators on bilattices.

Cyberinfrastructure is everywhere in diverse forms in service of applications in science, business and society. From IoT to extreme-scale computing data and computing have never been so distributed with the potential for real-time integration into these applications. The common theme to these applications, mostly composed of (big) data-integrated workloads, is their need to run in specialized environments for reasons such as on-demand or 24x7 nature of the tasks they are performing, and difficulties regarding their portability, latency, privacy, and performance optimization. Moreover, in many data-driven scientific applications, there is a need for heterogeneous integration of tasks requiring specialized computing capabilities with traditional high-throughput computing or high-performance computing tasks. Although some key middleware technologies enabled demonstration of standalone heterogeneous applications, such integration requires expertise convergence from a large group of people in very specialized settings. There are still many challenges for streamlined, scalable, repeatable, responsible, and explainable integration of data-integrated applications. Key opportunities for further innovations include intelligent systems and automated workflow management software that can compose and steer dynamic applications that can adapt to changing conditions in a data-driven fashion while integrating many tools to explore, analyze and utilize data. This talk will discuss some examples for data-integrated applications, describe emerging systems that enabled these applications, and overview our recent research to enable composable applications including a convergence application development methodology, intelligent middleware, and workflow composition.

Modern cloud computing workloads are becoming day by day more demanding, in terms of computational resources, as they feature multiple complex components, utilize heterogeneous hardware, and require tremendous amounts of memory. Such attributes of the emerging workloads disrupt the traditional design of cloud infrastructures, which are bound to decisions at the design time of the infrastructure, and mandate the dynamic composability of the next-generation cloud infrastructures.Scaling beyond the physical boundaries of the server trays, and minimizing over-provisioning of the nodes by disaggregating computational resources, such as CPUs, memory, etc., is a timely research problem. However, the prior line of research focuses on either NVM technologies or other disk-related approaches that try to relax the resource pressure induced by over-provisioning.In this work, we design, implement, and evaluate all necessary changes in the system software stack to support the dynamic allocation of disaggregated memory, depending on the needs of the workloads at hand. As a result, we can transparently increase the available memory of a system and achieve on average 57% better performance, compared to Swap, the de-facto mechanism used today for over-provisioning. Furthermore, we present a memory balancing policy that autonomously migrates memory pages across local and disaggregated memory. Our experimental results show that, even with a limited amount of local memory, memory balancing improves the performance by 41% on average, compared with using only disaggregated memory.

Detailed maps of the molecular basis of the disease are powerful tools for interpreting data and building predictive models. Modularity and composability are considered necessary network features for large-scale collaborative efforts to build comprehensive molecular descriptions of disease mechanisms. An effective way to create and manage large systems is to compose multiple subsystems. Composable network components could effectively harness the contributions of many individuals and enable teams to seamlessly assemble many individual components into comprehensive maps. We examine manually built versions of the RAS–RAF–MEK–ERK cascade from the Atlas of Cancer Signalling Network, PANTHER and Reactome databases and review them in terms of their reusability and composability for assembling new disease models. We identify design principles for managing complex systems that could make it easier for investigators to share and reuse network components. We demonstrate the main challenges including incompatible levels of detail and ambiguous representation of complexes and highlight the need to address these challenges.

We present a topology aware quantum synthesis algorithm designed to produce short circuits and to scale well in practice. The main contribution is a novel representation of circuits able to encode placement and topology using generic "gates", which allows the QFAST algorithm to replace expensive searches over circuit structures with few steps of numerical optimization. When compared against optimal depth, search based state-of-the-art techniques, QFAST produces comparable results: 1.19× longer circuits up to four qubits, with an increase in compilation speed of 3.6×. In addition, QFAST scales up to seven qubits. When compared with the state-of-the-art "rule" based decomposition techniques in Qiskit, QFAST produces circuits shorter by up to two orders of magnitude (331×), albeit 5.6× slower. We also demonstrate the composability with other techniques and the tunability of our formulation in terms of circuit depth and running time.

Robotic testbeds used for flight and research technology development are highly complicated electromechanical systems demanding large engineering effort to configure and manage safety-critical hardware. The software that interoperates with robotic testbeds needs to be robust yet flexible to accommodate rapidly changing testbed needs and other operational demands in a cost-efficient manner. The Jet Propulsion Laboratory (JPL) presents a new open-source C++ library called Fastcat for powerful and flexible EtherCAT device configuration for testbed and robotic applications. Fastcat implements a set of C drivers called ‘Just SOEM Drivers’ built on the popular Simple Open EtherCAT Master library for a small, but highly tested set of supported EtherCAT devices. Fastcat offers a rich set of capabilities such as supporting an arbitrary number of EtherCAT Masters, a YAML input configuration file, and a visualization tool ‘Fcviz’ to graph the bus topology using the open-source Graphiz library. Furthermore, a novel feature called ‘Fastcat Signals’ can efficiently route data and commands between devices to compose self-contained closed loop control systems such as heaters or joint-torque controllers with zero added latency. Abstract device types like signal generators, functions, and PID controllers and offline versions of device hardware drivers allow for powerful composability, offline-only testing, and flexible hybrid partial online – offline bus topologies. The Fastcat core library is middleware agnostic, but ROS2 wrappers are developed for ease-of-use. This paper will describe design tradeoffs, an overview of the implementation of these capabilities, and early results from the first JPL Robotic testbed use.

The aim of this focus letter is to present a comprehensive classification of the main entropic forms introduced in the last fifty years in the framework of statistical physics and information theory. Most of them can be grouped into three families, characterized by two-deformation parameters, introduced respectively by Sharma, Taneja, and Mittal (entropies of degree $(\alpha,\,\beta$)), by Sharma and Mittal (entropies of order $(\alpha,\,\beta)$), and by Hanel and Thurner (entropies of class $(c,\,d)$). Many entropic forms examined will be characterized systematically by means of important concepts such as their axiomatic foundations {\em \`{a} la} Shannon-Khinchin and the consequent composability rule for statistically independent systems. Other critical aspects related to the Lesche stability of information measures and their consistency with the Shore-Johnson axioms will be briefly discussed on a general ground., Comment: 14 pages, 6 tables, no figures, to appear on EPL: Focus Issues "Progresses on Statistical Physics and Complexity"

The chemical industry and subsequent value chain of plastics are facing significant challenges from the viewpoints of resource conversion and environmental burden. Now is the time to explore the future direction of plastics, which will require an integrated scheme using resource circulation, carbon neutrality, and a social system to promote after-use treatment under the concept of a circular economy. Polylactic acid (PLA) should help reduce greenhouse gas (GHG) emissions as a biobased material and contribute to waste management after use due to its biodegradability if managed properly. That is, it will be necessary to treat biodegradable products appropriately in closed systems such as composting facilities after use and recovery. To realize the implementation of fully approved composting facilities in society, simply evaluating biodegradability in the laboratory is insufficient. In this study, a pilot-scale test using PLA under actual composting conditions was conducted in accordance with both international standards and domestic evaluation methods. The results not only confirm its biodegradability and disintegration, but also demonstrate that the presence of a biodegradable plastic product has a negligible impact on the composting process. The obtained compost did not adversely affect plant germination or growth, demonstrating its safety and high quality. Such a multifaceted perspective makes this study unique and useful for creating a social framework.

Logical Execution Time (LET) is a timed programming abstraction, which features predictable and composable timing. It has recently gained considerable attention in the automotive industry, where it was successfully applied to master the distribution of software applications on multi-core electronic control units. However, the LET abstraction in its conventional form is only valid within the scope of a single component. With the recent introduction of System-level Logical Execution Time (SL LET), the concept could be transferred to a system-wide scope. This article improves over a first paper on SL LET, by providing matured definitions and an extensive discussion of the concept. It also features a comprehensive evaluation exploring the impacts of SL LET with regard to design, verification, performance, and implementability. The evaluation goes far beyond the contexts in which LET was originally applied. Indeed, SL LET allows us to address many open challenges in the design and verification of complex embedded hardware/software systems addressing predictability, synchronization, composability, and extensibility. Furthermore, we investigate performance trade-offs, and we quantify implementation costs by providing an analysis of the additionally required buffers.

Representing the semantics of GUI screens and components is crucial to data-driven computational methods for modeling user-GUI interactions and mining GUI designs. Existing GUI semantic representations are limited to encoding either the textual content, the visual design and layout patterns, or the app contexts. Many representation techniques also require significant manual data annotation efforts. This paper presents Screen2Vec, a new self-supervised technique for generating representations in embedding vectors of GUI screens and components that encode all of the above GUI features without requiring manual annotation using the context of user interaction traces. Screen2Vec is inspired by the word embedding method Word2Vec, but uses a new two-layer pipeline informed by the structure of GUIs and interaction traces and incorporates screen- and app-specific metadata. Through several sample downstream tasks, we demonstrate Screen2Vec's key useful properties: representing between-screen similarity through nearest neighbors, composability, and capability to represent user tasks., Accepted to CHI Conference on Human Factors in Computing Systems (CHI 2021)

Proving the security of masked implementations in theoretical models that are relevant to practice and match the best known attacks of the side-channel literature is a notoriously hard problem. The random probing model is a promising candidate to contribute to this challenge, due to its ability to capture the continuous nature of physical leakage (contrary to the threshold probing model), while also being convenient to manipulate in proofs and to automate with verification tools. Yet, despite recent progress in the design of masked circuits with good asymptotic security guarantees in this model, existing results still fall short when it comes to analyze the security of concretely useful circuits under realistic noise levels and with low number of shares. In this paper, we contribute to this issue by introducing a new composability notion, the Probe Distribution Table (PDT), and a new tool (called STRAPS, for the Sampled Testing of the RAndom Probing Security). Their combination allows us to significantly improve the tightness of existing analyses in the most practical (low noise, low number of shares) region of the design space. We illustrate these improvements by quantifying the random probing security of an AES S-box circuit, masked with the popular multiplication gadget of Ishai, Sahai and Wagner from Crypto 2003, with up to six shares.

Since the inception of Bitcoin, a plethora of distributed ledgers differing in design and purpose has been created. While by design, blockchains provide no means to securely communicate with external systems, numerous attempts towards trustless cross-chain communication have been proposed over the years. Today, cross-chain communication (CCC) plays a fundamental role in cryptocurrency exchanges, scalability efforts via sharding, extension of existing systems through sidechains, and bootstrapping of new blockchains. Unfortunately, existing proposals are designed ad-hoc for specific use-cases, making it hard to gain confidence in their correctness and composability. We provide the first systematic exposition of cross-chain communication protocols.

International audience; We present a composably secure protocol allowing $n$ parties to test an entanglement generation resource controlled by a possibly dishonest party. The test consists only in local quantum operations and authenticated classical communication once a state is shared among them and provides composable security, namely it can be used as a secure subroutine by $n$ honest parties within larger communication protocols to test if a source is sharing quantum states that are at least $\epsilon$-close to the GHZ state. This claim comes on top of previous results on multipartite entanglement verification where the security was studied in the usual game-based model. Here, we improve the protocol to make it more suitable for practical use in a quantum network and we study its security in the Abstract Cryptography framework to highlight composability issues and avoid hidden assumptions. This framework is a top-to-bottom theory that makes explicit any piece of information that each component (party or resource) gets at every time-step of the protocol. Moreover any security proof, which amounts to showing indistinguishability between an ideal resource having the desired security properties (up to local simulation) and the concrete resource representing the protocol, is composable for free in this setting. This allows us to readily compose our basic protocol in order to create a composably secure multi-round protocol enabling honest parties to obtain a state close to a GHZ state or an abort signal, even in the presence of a noisy or malicious source. Our protocol can typically be used as a subroutine in a Quantum Internet, to securely share a GHZ state among the network before performing a communication or computation protocol.

The term decentralized finance (DeFi) refers to an alternative financial infrastructure built on top of the Ethereum blockchain. DeFi uses smart contracts to create protocols that replicate existing financial services in a more open, interoperable, and transparent way. This paper highlights opportunities and potential risks of the DeFi ecosystem. I propose a multi-layered framework to analyze the implicit architecture and the various DeFi building blocks, including token standards, decentralized exchanges, decentralized debt markets, blockchain derivatives, and on-chain asset management protocols. I conclude that DeFi still is a niche market with certain risks but that it also has interesting properties in terms of efficiency, transparency, accessibility, and composability. As such, DeFi may potentially contribute to a more robust and transparent financial infrastructure. (JEL G15, G23, E59)

Decentralized financial (DeFi) applications on the Ethereum blockchain are highly interoperable because they share a single state in a deterministic computational environment. Stakeholders can deposit claims on assets, referred to as ‘liquidity shares’, across applications producing effects equivalent to rehypothecation in traditional financial systems. We seek to understand the degree to which this practice may contribute to financial integration on Ethereum by examining transactions in ‘composed’ derivatives for the assets DAI, USDC, USDT, ETH and tokenized BTC for the full set of 344.8 million Ethereum transactions computed in 2020. We identify a salient trend for ‘composing’ assets in multiple sequential generations of derivatives and comment on potential systemic implications for the Ethereum network.

Combat system modeling generally includes two aspects: structure and behavior. Structural modeling is to build the structure of entities and their internal and external static relationships. Behavioral modeling aims at the typical working processes. The simulation modeling definition language (SMDL) of Simulation Modeling Platform (SMP2) can describe system structure well, but it is difficult to support behavioral modeling. The modeling and simulation tool named Ptolemy is able to support the description of system behavior, but it lacks effective support for structural modeling. For this reason, the goal of the paper is to explore a mechanism to combine structural and behavioral modeling, which can not only effectively support the architecture design but also support the expression of system behaviors. As a proof of concept, we extend the SMDL by adding the synchronous data flow (SDF) elements, and use this new language, namely, the extended Simulation Model Definition Language (ESMDL), to specify a radar system for both of structural and behavioral modeling.

This publication is based on our paper presented at the IEEE International Conference on Software Architecture 2019. Due to their close interconnection with the outside world, cyber-physical systems are vulnerable to information leaks. Accordingly, it is crucial for software engineers to regulate and analyze the flow of information through systems. The microservice architectural style requires engineers to refine the regulations into security policies for the constituent software components. These policies must be composable to secure the information flow from end to end. However, since security is hard to compose, a composition of secure components may lead to an insecure system. In our paper, we enable microservice architectures of cyber-physical systems to be composed securely. First, we provide engineers with a set of architectural well-formedness rules for the refinement of security policies, ensuring composability if the constituent components communicate by message passing. Second, we present a verification technique to analyze whether the real-time message passing of components adheres to their refined security policies. Since the analysis results are securely composable, we assure engineers that a composition of secure components will always lead to a secure system. We evaluated the accuracy of our contributions using an extension of the CoCoME case study.

One of the benefits of decentralized finance (DeFi) – an alternative financial system built on blockchain – is composability, which means the system’s building blocks (tokens) can freely interact with one another to form new services. One example is stablecoin, a token with fixed exchange rate, which is backed by token collaterals. While stablecoins can be used to facilitate payments and exchanges, in DeFi they can be used to earn returns (“yield farming”), potentially multiplicatively. We use transaction-level blockchain data to analyze a stablecoin’s flows between protocols and provide suggestive evidence of DeFi yield-chasing behavior. We shed light on what DeFi total value locked might really measure and highlight the complexity in DeFi analysis and market surveillance.

International audience; The probing security model is widely used to formally prove the security of masking schemes. Whenever a masked implementation can be proven secure in this model with a reasonable \emph{leakage rate}, it is also provably secure in a realistic leakage model known as the \emph{noisy leakage model}. This paper introduces a new framework for the composition of probing-secure circuits. We introduce the security notion of \emph{input-output separation} (IOS) for a refresh gadget. From this notion, one can easily compose gadgets satisfying the classical probing security notion --which does not ensure composability on its own-- to obtain a \emph{region probing secure} circuit. Such a circuit is secure against an adversary placing up to $t$ probes in each gadget composing the circuit, which ensures a tight reduction to the more realistic noisy leakage model. After introducing the notion and proving our composition theorem, we compare our approach to the composition approaches obtained with the (Strong) Non-Interference (S/NI) notions as well as the Probe-Isolating Non-Interference (PINI) notion. We further show that any uniform SNI gadget achieves the IOS security notion, while the converse is not true. We further describe a refresh gadget achieving the IOS property for any linear sharing with a quasilinear complexity $\Theta(n \log n)$ and a $O(1/\log n)$ leakage rate (for an $n$-size sharing). This refresh gadget is a simplified version of the quasilinear SNI refresh gadget proposed by Battistello, Coron, Prouff, and Zeitoun (ePrint~2016). As an application of our composition framework, we revisit the quasilinear-complexity masking scheme of Goudarzi, Joux and Rivain (Asiacrypt~2018). We improve this scheme by generalizing it to any base field (whereas the original proposal only applies to field with $n$th powers of unity) and by taking advantage of our composition approach. We further patch a flaw in the original security proof and extend it from the random probing model to the stronger region probing model. Finally, we present some application of this extended quasilinear masking scheme to AES and MiMC and compare the obtained performances.

A significant aspect of software integrity is the ability to determine whether a system is correctly showing the information it is intended to show. This work combines abstract cryptographic composability principles with automated machine learning techniques to support a new methodology for software integrity checking, particularly in the intractable domain of interface validation. A subtle but often perilously overlooked cryptographic principle is the requirement that a sender be aware of the meaning of inputs, specifically of the cleartext behind encrypted messages. We propose using computer vision to evaluate whether interfaces exhibit technical awareness of information content, enabling automated development-time and real-time integrity checking that is far more efficient and extensive than manual analysis.

A simulation System of Systems (SoS) comprised of various simulation systems may have dissimilar modeling paradigms. For performing autonomy research and development, various types of simulation systems need to be brought together to build a multi-domain virtual SoS wherein effects of autonomous entities/agents can be observed. While the distributed simulation community has solved the integrability challenge using standards like Distributed Interactive Simulation (DIS) or High Level Architecture (HLA), the model composability challenge is an open research problem. Many software/systems can now be made available as docker applications which can be readily plugged into existing simulation systems. However, the trust issues with such integration limit their usage as established systems cannot trust third party apps. This paper highlights some of the challenges with building a cloud-based simulation SoS, proposes an architecture framework using the concept of structural autonomy and leverages Modeling & Simulation as a fundamental key enabler for autonomy research.

To implement Service Oriented Architecture (SOA) in a banking company for transactional banking activity, this paper aims to overcome the problem of several related surrounding systems which has the same function in the different system by using Domain Driven Design. The paper proposes an approach to SOA using Web Services for service delivery in the area of transactional banking activities. Several systems will be connected to a BUS that will wait on and manage any request coming from other applications. To design the system then in this paper also will identify which application will consume the same function and analyze which function belongs to a certain domain. The paper finds that the implementation of an SOA system for transactional banking activities can be achieved by rapidly changing the habit of scaling up the system and application. This study shows that banking activity has a huge number of systems that should sync one and another to maintain the data integrity, availability, interoperability, and composability of the system.

This article explores the metaphor of Science as provider of sharp images of ourenvironment, using the epistemological framework of Objective Cognitive Constructivism.These sharp images are conveyed by precise scientific hypotheses that, in turn, are encodedby mathematical equations. Furthermore, this article describes how such knowledge is pro-duced by a cyclic and recursive development, perfection and reinforcement process, leadingto the emergence of eigen-solutions characterized by the four essential properties of preci-sion, stability, separability and composability. Finally, this article discusses the role playedby ontology and metaphysics in the scientific production process, and in which sense theresulting knowledge can be considered objective.

Many-core platforms are rapidly expanding in various embedded areas as they provide the scalable computational power required to meet the ever-growing performance demands of embedded applications and systems. However, the huge design space of possible task mappings, the unpredictable workload dynamism, and the numerous non-functional requirements of applications in terms of timing, reliability, safety, and so forth. impose significant challenges when designing many-core systems. Hybrid Application Mapping (HAM) is an emerging class of design methodologies for many-core systems which address these challenges via an incremental (per-application) mapping scheme: The mapping process is divided into (i) a design-time Design Space Exploration (DSE) step per application to obtain a set of high-quality mapping options and (ii) a run-time system management step in which applications are launched dynamically (on demand) using the precomputed mappings. This paper provides an overview of HAM and the design methodologies developed in line with it. We introduce the basics of HAM and elaborate on the way it addresses the major challenges of application mapping in many-core systems. We provide an overview of the main challenges encountered when employing HAM and survey a collection of state-of-the-art techniques and methodologies proposed to address these challenges. We finally present an overview of open topics and challenges in HAM, provide a summary of emerging trends for addressing them particularly using machine learning, and outline possible future directions. While there exists a large body of HAM methodologies, the techniques studied in this paper are developed, to a large extent, within the scope of invasive computing. Invasive computing introduces resource awareness into applications and employs explicit resource reservation to enable incremental application mapping and dynamic system management., publishedVersion

Owing to the results of research in system science, artificial intelligence, and cognitive engineering, engineered systems are becoming more and more powered by knowledge. Complementing common-sense and scientific knowledge, system knowledge is maturing into a crucial productive asset. However, an overall theory of the knowledge of intellectualized systems does not exist. Some researchers suggest that time has come to establish a philosophically underpinned theoretical framework. This motion is seconded by the on-going intelligence revolution, in which artificial intelligence becomes a productive power, enabler of smart systems, and a strong transformer of the social life. The goal of this paper is to propose a skeleton of the needed generic theory of system knowledge (and a possible new branch of philosophical studies). The major assumption is that a significant part of the synthetic system knowledge (SSK) is &ldquo, symp&eacute, rasma&rdquo, that is, knowledge conjectured, inferred, constructed, or otherwise derived during the operation of systems. This part will become even more dominant in the future. Starting out from the above term, the paper suggests calling this theory &ldquo, rasmology&rdquo, Some specific domains of &ldquo, rasmological&rdquo, studies, such as (i) manifestations of SSK, (ii) mechanisms of generating SSK, (iii) dependability of SSK, (iv) operational power of SSK, (v) composability of SSK, and (vi) advancement of SSK, are identified. It is understood that the essence and status of SSK cannot be investigated without considering the related cognitive processes and technological enablers. The paper presents a number of open questions relevant for follow-up discussions.

There are multiple steps involved in transitioning a server from the factory to being fully provisioned for an intended workload. These steps include finding the optimal slot for the hardware and to compose the required resources on the hardware for the intended workload. There are many different factors that influence the placement of server hardware in the datacenter, such as physical limitations to connect to a network be it Ethernet or storage networks, power requirements, temperature/cooling considerations, and physical space, etc. In addition to this, there may be custom requirements driven by workload policies (such as security, data privacy, power redundancy, etc.). Once the server has been placed in the right slot it needs to be configured with the appropriate resources for the intended workload. CIED will provide a ranked list of locations for server placement based on the intended workload, connectivity and physical requirements of the server. Once the server is placed in the suggested slot, the solution automatically discovers the server and composes the required resources (compute, storage and networks) for running the appropriate workload. CIED reduces the overall time taken to move hardware from factory to production and also maximizes the server hardware utilization while minimizing downtime by physically placing the resources optimally. From the case study that was undertaken, the time taken to transition a server from factory to being fully provisioned was proportional to the number of devices in the datacenter. With CIED this time is constant irrespective of the complexity or the number of devices in a datacenter.

International audience; Component-based software engineering is a paradigm that fosters software flexibility and emphasizes composability and reuse of software components. These are runtime units that provide services and, in turn, may require other services to operate. Assembling components consists in binding compo-nents' required services to provided ones to deliver composite services with added value. Building a composite service is a challenging task as it requires identifying components and services that are compatible, binding them to implement the service, and describe it for discovery. For that, the vocabulary used to describe component-based services (i.e., services offered by components or assemblies) must support the description of required services, and descriptions must be combinable in order to automatically generate composite service descriptions. However, existing solutions are limited to the description and composition of provided (and not required) services. In this paper, we consider ontologies to describe component-based services implemented by component assemblies. After comparing existing service ontologies, we present an extension of OWLS called Comp-O. Through a proof-of-concept, we demonstrate how the added semantics can be handled to automatically build composite service descriptions.

Current trends in High Performance Computing suggest a significant shift towards heterogeneous architectures, utilising GPUs and other accelerators for their combination of computation capacity and power efficiency. Therefore, programming heterogeneous applications becomes increasingly relevant. However, the programming models for accelerators may present challenges that render the development process difficult and require extra effort from developers to handle tha parallelisation issues. OpenACC is a directive-based programming model aiming to facilitate the development of heterogeneous applications, abstracting the accelerator specific details from the programmer. OmpSs-2 is a directive-based, task parallel programming model, designed to ease the development of parallel programs. It is also extendable, in order to support heterogeneity. This work explores the composability of the two programming models, proposes and implements a new feature in the OmpSs-2 model, supporting hybrid OmpSs-2 + OpenACC programs. The two models act complementary to each other, with OmpSs-2 providing task-parallelism and OpenACC handling data-parallelism. Both being directive-based, they present the potential to provide a consistent, flexible and productive parallel programming framework when combined. The resulting new feature has been part of the latest OmpSs-2 release.

Microservices architecture has become one of the most prominent software architectures in the software development processes due to its features such as scalability, maintainability, resilience, and composability. It allows developing business applications in a decentralized manner by dividing the important business logic into separate independent services. Digital certificates are used to verify the identity of microservices in most cases. However, the certificate authorities (CA) who issue the certificates to microservices cannot be trusted always since they can issue certificates without the consent of the relevant microservice. Nevertheless, existing implementations of certificate transparency are mostly centralized and has the vulnerability of the single point of failure. The distributed ledger technologies such as blockchain can be used to achieve decentralized nature in certificate transparency implementations. A blockchain-based decentralized certificate transparency system specified for microservices architecture is proposed in this paper to ensure secure communication among services. After the implementation and deployment in a cloud service, the system expressed average certificate querying time of 643 milliseconds along with the highly secured service provided.

We address energy-efficient placement of data and analytics components of composite analytics services on a wireless network to minimize execution-time energy consumption (computation and communication) subject to compute, storage and network resource constraints.We introduce an expressive analytics service hypergraph model for representing k-ary composability relationships (k ≥ 2) between various analytics and data components and leverage binary quadratic programming (BQP) to minimize the total energy consumption of a given placement of the analytics hypergraph nodes on the network subject to resource availability constraints. Then, after defining a potential energy functional Φ(•) to model the affinities of analytics components and network resources using analogs of attractive and repulsive forces in physics, we propose a decentralized Metropolis Monte Carlo (MMC) sampling method which seeks to minimize Φ by moving analytics and data on the network. Although Φ is non-convex, using a potential game formulation, we identify conditions under which the algorithm provably converges to a local minimum energy equilibrium placement configuration.Trace-based simulations of the placement of a deep-neural-network analytics service on a realistic wireless network show that for smaller problem instances our MMC algorithm yields placements with total energy within a small factor of BQP and more balanced workload distributions; for larger problems, it yields low-energy configurations while the BQP approach fails.

Medicine is moving from a curative discipline to a preventative discipline relying on personalised and precise treatment plans. The complex and multi level pathophysiological patterns of most diseases require a systemic medicine approach and are challenging current medical therapies. On the other hand, computational medicine is a vibrant interdisciplinary field that could help move from an organ-centered approach to a process-oriented approach. The ideal computational patient would require an international interdisciplinary effort, of larger scientific and technological interdisciplinarity than the Human Genome Project. When deployed, such a patient would have a profound impact on how healthcare is delivered to patients. Here we present a computational patient model that integrates, refines and extends recent mechanistic or phenomenological models of cardiovascular, RAS and diabetic processes. Our aim is twofold: analyse the modularity and composability of the model-building blocks of the computational patient and to study the dynamical properties of well-being and disease states in a broader functional context. We present results from a number of experiments among which we characterise the dynamic impact of COVID-19 and type-2 diabetes (T2D) on cardiovascular and inflammation conditions. We tested these experiments under different exercise, meal and drug regimens. We report results showing the striking importance of transient dynamical responses to acute state conditions and we provide guidelines for system design principles for the inter-relationship between modules and components in systemic medicine. Finally this initial computational Patient can be used as a toolbox for further modifications and extensions., 37 pages

International audience; We propose a compositional specification theory for reason- ing about components that interact by synchronisation of input and out- put (I/O) actions, in which the specification of a component constrains the temporal ordering of interactions with the environment. Such a the- ory is motivated by the need to support composability of components, in addition to modelling environmental assumptions, and reasoning about run-time behaviour. Models can be specified operationally by means of I/O labelled transition systems augmented by an inconsistency predi- cate on states, or in a purely declarative manner by means of traces. We introduce a refinement preorder that supports safe-substitutivity of components. Our specification theory includes the operations of parallel composition for composing components at run-time, logical conjunction for independent development, and quotient for incremental development. We prove congruence properties of the operations and show correspon- dence between the operational and declarative frameworks.

Complex simulation systems often comprise multiple distributed simulators that need to interoperate and synchronize states and events. In many cases, the simulation logics which are developed by different teams with specific expertise, need to be integrated to build a complete simulation system. Thus, supporting composability and reusability of simulation functionalities with minimal integration and performance overhead is a challenging but required capability. Middleware for game engines are promising to realize both the modular and reusable development criteria as well as the high performance requirements, while data-centric publish/subscribe middleware can support seamless integration and synchronization of the distributed artifacts. However, differences in the level of abstraction at which these middleware operate and the semantic differences in their underlying ontologies make it hard and challenging for simulation application developers and system integrators to realize a complete, operational system. To that end this paper presents a model-driven approach to blending the two middleware, wherein the modeling capabilities provide intuitive and higher-level abstractions for developers to reason about the composition and validation of the complete system, and the generative capabilities address the inherent and accidental complexities incurred in reconciling the semantic differences between the gaming and pub/sub middleware. We present a concrete implementation of our approach and illustrate its use and performance results using simple use cases.

We propose an entanglement-based quantum bit string commitment protocol whose composability is proven in the random oracle model. This protocol has the additional property of preserving the privacy of the committed message. Even though this property is not resilient against man-in-the-middle attacks, this threat can be circumvented by considering that the parties communicate through an authenticated channel. The protocol remains secure (but not private) if we realize the random oracles as physical unclonable functions in the so-called bad PUF model with access before the opening phase., Comment: 8 pages, 4 figures

In this paper, a model-driven software collaborative modeling method is proposed, and a software collaborative modeling framework on model assembly and model updating is established. The composability of models, the integrity of model assembly and the consistency of model updating are studied from two aspects: model assembly mechanism and model updating mechanism. The collaborative modeling protocol is defined, and six collaborative relationship stereotypes are introduced to add collaborative semantics to the model based on the extensible mechanism of UML. The algorithm of model assembly and integrity checking is proposed and the collaborative modeling of multiple clients is implemented. The algorithm of model updating and consistency checking is proposed to solve the problem of model updating in collaborative modeling.

One oft-endeavored security property for cryptographic hash functions is collision resistance: it should be computationally infeasible to find distinct inputs \(x,x'\) such that \(H(x) = H(x')\), where H is the hash function. Unruh (EUROCRYPT 2016) proposed collapseability as its quantum equivalent. The Merkle-Damgard and sponge hashing modes have recently been proven to be collapseable under the assumption that the underlying primitive is collapseable. These modes are inherently sequential. In this work, we investigate collapseability of tree hashing. We first consider fixed length tree hashing modes, and derive conditions under which their collapseability can be reduced to the collapseability of the underlying compression function. Then, we extend the result to two methods for achieving variable length hashing: tree hashing with domain separation between message and chaining value, and tree hashing with length encoding at the end of the tree. The proofs are performed using the collapseability composability framework of Fehr (TCC 2018), that allows us to discard of deeply technical quantum details and to focus on proper composition of the tree hashes from their compression function.

In recent years, misinformation on the Web has become increasingly rampant. The research community has responded by proposing systems and challenges, which are beginning to be useful for (various subtasks of) detecting misinformation. However, most proposed systems are based on deep learning techniques which are fine-tuned to specific domains, are difficult to interpret and produce results which are not machine readable. This limits their applicability and adoption as they can only be used by a select expert audience in very specific settings. In this paper we propose an architecture based on a core concept of Credibility Reviews (CRs) that can be used to build networks of distributed bots that collaborate for misinformation detection. The CRs serve as building blocks to compose graphs of (i) web content, (ii) existing credibility signals –fact-checked claims and reputation reviews of websites–, and (iii) automatically computed reviews. We implement this architecture on top of lightweight extensions to Schema.org and services providing generic NLP tasks for semantic similarity and stance detection. Evaluations on existing datasets of social-media posts, fake news and political speeches demonstrates several advantages over existing systems: extensibility, domain-independence, composability, explainability and transparency via provenance. Furthermore, we obtain competitive results without requiring finetuning and establish a new state of the art on the Clef’18 CheckThat! Factuality task.

Following the same trend of consumer electronics, safety-critical industries are starting to adopt Over-The-Air Software Updates (OTASU) on their embedded systems. The motivation behind this trend is twofold. On the one hand, OTASU offer several benefits to the product makers and users by improving or adding new functionality and services to the product without a complete redesign. On the other hand, the increasing connectivity trend makes OTASU a crucial cyber-security demand to download latest security patches. However, the application of OTASU in the safety-critical domain is not free of challenges, specially when considering the dramatic increase of software complexity and the resulting high computing performance demands. This is the mission of UP2DATE, a recently launched project funded within the European H2020 programme focused on new software update architectures for heterogeneous high-performance mixed-criticality systems. This paper gives an overview of UP2DATE and its foundations, which seeks to improve existing OTASU solutions by considering safety, security and availability from the ground up in an architecture that builds around composability and modularity. The research presented throughout this paper has received funding from the European Community’s Horizon 2020 programme under the UP2DATE project (grant agreement 871465).

The concept of cellular automata is one of the cornerstones of scientific and engineering pursuit with wide applicability in various domains. The rise of system complexity points to developing frameworks that can aid in developing composable models at multiple spatiotemporal levels. Toward this goal, an input/output mod-ular discrete-event cellular automata framework based on the Discrete Event System Specification (DEVS) is proposed. It is adapted from a Composable Cellular Automata (CCA) formalism that is defined in terms of a multicomponent discrete time system specification. The resulting Composable Cellular Automata DEVS (CCA-DEVS) framework is built using the Cellular Automata DEVS that is a part of the DEVS-Suite simulator. The approach and realization of the proposed CCA-DEVS framework are detailed. The framework is used to develop an example model composed of CCA-DEVS agent and partial differential equation models.