Gianluca Roascio
email: gianluca.roascio@polito.it

Gabriele Costa
email: gabriele.costa@imtlucca.it

Emmanuel Baccelli
email: emmanuel.baccelli@inria.fr

Lukas Malina
email: malina@vut.cz

Raimundas Matulevi Čius
email: raimundas.matulevicius@ut.ee

Marius Momeu
email: momeu@sec.in.tum.de

Nerijus Morkevi Čius
email: nerijus.morkevicius@ktu.lt

Enrico Russo
email: enrico.russo@unige.it

BRANKA STOJANOVI Ć9 Aimilia Tasidou
email: aimilia.tasidou@telecom-sudparis.eu

HArMoNICS: High-Assurance Microgrid Network Infrastructure Case Study

Keywords: security, cybersecurity, embedded systems, intelligent infrastructure, case study I

Modern Intelligent Infrastructures (II) are highly complex, interconnected systems that are now emerging. For instance, II can integrate technologies and processes to provide citizens with faster services and better goods. An average II can include many technologies, e.g., Cloud applications and IoT devices, under different environments, e.g., industry 4.0 production plants and smart buildings. Although II bring concrete benefits to all of these contexts, they also carry security concerns. Reasoning about threats and security exposures that might affect II is non trivial. This is only partially due to their inherent complexity. As a matter of fact, real II are typically in charge of some critical operations that cannot be interrupted or compromised for experimental purposes. An alternative solution is to rely on digital replicas which can provide a good trade off between realism and usability. These assets represent a strategic and highly demanded resource for the security community. In this paper we present HArMoNICS, a case study infrastructure meant to provide a playground for security experts interested in II security. HArMoNICS revolves around a digital replica of a real Smart Polygeneration Microgrid (SPM) located in Italy. Although most of the components are based on or inspired to the real system, HArMoNICS has been enriched with further security-relevant features. As a result, the case study includes vertical uses cases focusing on specific security topics. Security researchers can use it to assess the effectiveness of new methodologies, to carry out security training activities, or even to extend it with new elements.

applicable to II. A reason is that these infrastructures are extremely complex and heterogeneous, made of myriads of objects using hardware and software of many different manufacturers. Such an extreme diversity, together with the quick development of modern technologies, requires appropriate countermeasures to ensure the security of the next-generation II.

A growing trend is that of using Security-by-Design (S×D) [START_REF] Santos | A catalog of security architecture weaknesses[END_REF] as the leading principle. In short, S×D enriches the traditional development lifecycle with security-specific tasks. These tasks take place at every stage, from the very early design to the final deployment. By integrating these tasks in the development workflow, the S×D approach creates a security management process where every critical event triggers effects along the entire lifecycle. As a practical example, consider the case of a new vulnerability discovered in an existing II. Such a vulnerability may occur due to a design weakness, which one might want to evaluate against the initial security specifications. At the same time, the vulnerability may trigger the development of countermeasures, e.g., an emergency patch, as well as new security tests.

Although the ideas behind S×D and its potential benefits are clear, implementing it is still a major challenge. As a matter of fact, all the security tasks previously mentioned must be implemented and populated with actual security tools and procedures. For each of them, many alternatives exist and new ones appear over time. As a consequence, the entire security workflow must be continuously revised and maintained. Even worse, assessing the actual effectiveness of the involved security procedures is hardly feasible. For instance, most of these procedures require discontinuing the operations of the II, which is typically infeasible. Hence, the actual effectiveness of the processes it often only accessed when a real security event occurs and, if they fail, when it is too late.

A possible solution for the assessment of S×D frameworks is to rely on II replicas. For instance, computer simulations can accurately reproduce the behavior of a real system. However, virtual II are rarely available. A reason is that, although simplified, they typically bring part of the complexity of a real II. Thus, they are often considered a valuable asset by private actors who may prefer not to be shared. Furthermore, when they are created to mimic a real II, they may lack the security aspects of interest, e.g., vulnerabilities, for assessing the effectiveness of security solutions.

In this paper, we present our High-Assurance Microgrid Network Infrastructure Case Study (HArMoNICS), developed within the EU project SPARTA. 1 Briefly, HArMoNICS revolves around a zero-emission building scenario in the context of a smart microgrid. All the elements appearing in our case study are taken from or inspired by actual systems that reside inside the original infrastructure.

The main motivation behind our proposal is the strategic role of intentionally vulnerable environments, which provide 1 www.sparta.eu a shared setting for research and development of security techniques. Indeed, such environments stimulate and favor innovation by providing a touchstone for new methodologies. The main goal of HArMoNICS is to be a valuable asset for the community interested in the security and privacy of critical and intelligent infrastructures. Researchers can use it both as a playground, e.g., for hosting training exercises, and as a benchmark, e.g., for systematically assessing the effectiveness of a certain security mechanism under different scenarios. These activities can be carried out by taking advantage of the built-in use cases. Furthermore, new use cases can be added to model specific security concerns, e.g., related to new technologies. Finally, through a VPN-based integration mechanism, physical devices can be plugged in, and dually, HArMoNICS can be used to extend existing environments, such as simulators or digital twins.

In summary, among the features of HArMoNICS, the following ones are those we consider highly relevant for the security community.

• The case study is designed and implemented in order to mimic a real II, and therefore it includes a number of technologies that may appear within the perimeter of a smart infrastructure. • The entire case study can be executed inside a publiclyavailable virtual machine, with minimal computational resources.

The rest of this paper is organized as follows. Section II describes the general features of architecture and networking related to the case study infrastructure. Section III details every single scenario included, with the relative security and privacy problem statement. Section IV offers a glimpse of the current state of the art in such a kind of digital replicas. Finally, Section V concludes the paper.

II. ARCHITECTURE OVERVIEW

The HArMoNICS case study is based on a smart building scenario, composed of both IT and OT elements. The scenario is inspired to the Zero-Emission Building (ZEB), which is hosted inside the Genoa University Campus, located in Savona (Italy). Figure 1 shows a sky view of the Campus, with the ZEB location highlighted in red. Among the research infrastructures and facilities that the Campus hosts, there is a smart grid, called Savona Polygeneration Microgrid (SPM), consisting of several nodes for the generation of power. Power generation nodes rely on different sources, e.g., solar panels and gas turbines, and their production partially supplies the internal energy demand. ZEB is a smart building where innovative technologies and materials are adopted in order to optimize the energy consumption with the ultimate goal of nullifying the carbon footprint. It contains several laboratories, offices and a gym. Some servers and networks reside in the building and they host the services which contribute to the IT infrastructure. Standard and Fog-enabled access points provide wireless connectivity to network devices, including IoT ones. Also, sensors and actuators have been deployed to monitor the environment (e.g., room temperature) and reconfigure it (e.g., by opening a window).

A. NETWORK INFRASTRUCTURE

The network infrastructure of HArMoNICS is here described in more details. Figure 2 shows the reference network scheme of the case study. Briefly, the smart building hosts a threesegment network. The three segments are dmz, intranet and iot. Servers hosting public services, i.e., those that are accessible from outside the network perimeter, are connected to dmz. Other servers, instead, and hosts are connected to intranet. Finally, iot is used for connecting various field devices, e.g., sensors, actuators, and Fog nodes. The smart building network resides behind a router firewall that delimits the perimeter with the external network, i.e., the public Internet.

Networks and nodes are labeled with their symbolic names, e.g., ns and www, and IP addresses. Node names are managed by the DNS service running on node ns. Network address space represents the interval of IP addresses that can be assigned to connected devices. For brevity, statically assigned IPs are only represented by the last address segments. For instance, the IP address of node www is 198.51.100.3. If a node has no address label, its IP address is dynamically assigned. Finally, when relevant, connections are labeled with a specification of the used channel, e.g., IEEE 802.15.4.

The colored and numbered circles indicate that the nearby devices belong to one of the 8 security and privacy-related scenarios described, which will be detailed in the next Section.

The network topology described above is implemented by means of Docker containers and networks [START_REF] Docker | What is a Container? -App Containerization[END_REF]. Roughly speaking, Docker containers are lightweight virtual machines running inside isolated Linux processes. Container connectivity is granted by means of virtual networks which are emulated by the host machine.

Figure 3 highlights the implementation details of the network infrastructure of HArMoNICS. Below, the core aspects are discussed.

• Public network simulation. Several devices connect with the scenario infrastructure by means of the public Internet (see Figure 2). Some of them are actual, remote entities (e.g., web servers), while others must be deployed within the scenario. To support this hybrid structure, the infrastructure relies on a simulated internet (Figure 3). The simulated internet is implemented by means of a router (rt-simint) which connects three networks, i.e., ext, simint and outside. Briefly, ext is connected with a virtual interface of the host platform. By means of a virtual bridge, the host interface provides direct connectivity with the real Internet. • VPN access. To make the infrastructure extensible, direct access to each network is provided, by means of a virtual private network (VPN) server. The VPN server is connected to ext. In this way, the VPN can be accessed from software running on the host platform and even from the Internet. The server accepts connections on different ports, in the range [8886 -8889]. Each port is uniquely mapped into one of the network in the infrastructure. In Figure 3, port numbers are used to label (in red) the connection with the corresponding network. For instance, establishing a session with 172.16.255.100:8886 will connect the VPN client to the intranet. HArMoNICS has been designed with a standard Infrastructure-as-Code (IaC) framework called TOSCA [START_REF] Lipton | TOSCA Simple Profile in YAML Version 1.3[END_REF]. Docker Compose [START_REF] Documentation | Overview of Docker Compose[END_REF], the default Docker orchestrator, has been chosen as scenario deployment tool. Finally, the scenario code is hosted on a Github repository at https://github. com/enricorusso/spartawp6. In this way, by deploying HAr-MoNICS from the Github repository, continuous integration is also supported.

III. USE CASES

This Section provides a glimpse of the main use cases included in HArMoNICS. Each of the scenarios focuses on a different security concern and refers to a subsystem within the case study infrastructure. Furthermore, for each scenario, we carry out a discussion of open challenges and possible countermeasures that are being investigated in the context of the SPARTA project. The discussed techniques are relevant to highlight how security researchers can leverage on HArMoNICS for assessing their methodologies in a realistic setting.

A. SOFTWARE INTEGRITY FOR SMART SENSORS

One of the main threats to the security of II is the limited, or even absent, protection of the sensing devices that often form a significant part of the perimeter of the entire infrastructure. For example, the smart door sensor, placed within the iot network, has the task of monitoring the access of individuals inside the building (item 1 in Figure 2, in cyan). To do this, it pairs over Bluetooth with the mobile device of the person accessing, and requests the transmission of a unique identifier. An app is installed on the personal device, capable of interacting with the door sensor to pass it the person ID.

Given the reduced operation complexity and the low activation frequency, the door sensor is an embedded device on which a firmware written in C language runs on baremetal. C language permits low-level control without losing the advantages of high-level statements and data structures. Still, the manual management of data structures and memory pointers is often a source of vulnerabilities. The lack of mem- Reasonably, the most famous vulnerability for this scenario is buffer overflow [START_REF]Improper Restriction of Operations within the Bounds of a Memory Buffer[END_REF], which is caused by increasing or decreasing a pointer without proper boundary checks on the data structure that is being accessed. This results in outof-bounds writes that corrupt adjacent data areas, e.g., stack or heap. Similar problems may arise when indexing bugs are present in the code, i.e., boundary checks over an index for a given data structure are missing or incomplete. Indexing bugs are often caused by integer-related errors like an integer overflow, truncation or signedness bugs, or incorrect pointer casting.

In the present use case, the firmware may mistakenly consider the mobile app as a trusted actor. In particular, since the transmitted information has a fixed size in bytes, the sensor may not check the incoming messages, but just read bytes until the string termination symbol is received. An attacker can exploit this vulnerability in various ways, e.g., to steal data or enter the network. Moreover, this vulnerability is an enabling factor for, e.g., bypassing a possible non-executable-stack defense [START_REF] Docs | Data Execution Prevention -Win32 apps[END_REF], and mounting a Return-Oriented Programming (ROP) attack [START_REF] Roemer | Return-oriented programming: Systems, languages, and applications[END_REF] [12] [START_REF] Weidler | Returnoriented programming on a resource constrained device[END_REF].

Discussion

A possible solution to preserve control-flow integrity in unprotected devices is by using enforcement mechanisms, e.g., relying on security extensions that consist of adopting a runtime Policy Decision Point (PDP), also called controlflow monitor, and several Policy Enforcement Points (PEPs), inserted before runtime into the code. Because of the small capabilities of these devices, this extension must be as tiny as possible in terms of additional computational resources, and must not compromise the real-time nature of the execution. An example is given by [START_REF] Maunero | A FPGA-based Control-Flow Integrity Solution for Securing Bare-Metal Embedded Systems[END_REF], where a lightweight solution is presented to protect firmware running on a microcontroller through the use of an external FPGA, which implements a checker. Checks are triggered at critical branch points by a single instruction that invokes the FPGA. Here, the legitimacy of the control-flow transfer is checked through a completely parallel execution, and if necessary, CPU activity is interrupted if a violation is detected.

B. SOFTWARE UPDATE FOR IOT END DEVICES

Low-power indoor sensors (AirMonitors) continuously collect data about the air quality inside the ZEB, aiming to detect and prevent bad air quality situations, which could lead, e.g., to a higher risk of COVID transmission.

From the hardware point of view, the AirMonitor prototype present in HArMoNICS bundles a typical COTS System-on-Chip (SoC): an ARM Cortex-M microcontroller communicating with IEEE 802.15.4 low-power radio. This SoC is connected via I2C/SPI bus on-board to a variety of sensors, for humidity, gas, and dust particles. The AirMonitor is networked via a low-power wireless access point, through which it communicates via IP protocols (6LoWPAN and CoAP) with a remote software udpate server (items 2 in Figure 2, in red). The software embedded on AirMonitors is based on RIOT [START_REF] Baccelli | RIOT: An open source operating system for low-end embedded devices in the IoT[END_REF], a popular open-source general-purpose operating system for low-power IoT devices.

The idea behind this scenario is to offer a test case for the security of software updates for low-power IoT devices. Over the last few years, the research community has been working on the definition of several IoT update processes [START_REF] Kolehmainen | Secure Firmware Updates for IoT: A Survey[END_REF], among which secure software updates for resourceconstrained devices is a challenging research topic [START_REF] Acosta Padilla | The Future of IoT Software Must be Updated[END_REF].

Discussion

The Internet Engineering Task Force (IETF) is currently on defining a new standard for firmware updates called Software Updates for Internet of Things (SUIT) [START_REF]Website of : IETF SUIT draft architecture[END_REF] [START_REF] Moran | A Concise Binary Object Representation (CBOR)-based Serialization Format for the Software Updates for Internet of Things (SUIT) Manifest[END_REF]. The main goals of SUIT are interoperability and end-to-end security. The SUIT information model [START_REF] Ietf | Website of : Firmware updates for internet of things devices -an information model for manifests draft-ietf-suit-information-model-03[END_REF] defines a collection of security threats for the update process. Threats associated with this type of scenario are manifold. As discussed in [START_REF] Zandberg | Secure Firmware Updates for Constrained IoT Devices Using Open Standards: A Reality Check[END_REF], an attacker might update the IoT device with a modified and intentionally flawed firmware image. Alternatively, an attacker may replay a valid, but old (known-to-be-flawed) firmware, or a firmware update that is authentic, but for an incompatible device.

Although the SUIT model suggests a set of security requirements and countermeasures, it is worth noticing that all these threats are related to the integrity and the confidentiality of the update process only, while the content of the update is assumed to be trusted. Therefore, the SUIT workflow allows an Information System Management (ISM) service to upload a firmware image containing security vulnerabilities or malicious behaviors. Furthermore, as demonstrated by some recent work, the SUIT workflow is flexible in that it allows not only pre-quantum, but also post-quantum security [START_REF] Banegas | Quantum-Resistant Security for Software Updates on Low-power Networked Embedded Devices[END_REF], and does not only cater for full IoT firmware updates, but also for securing modular software updates on low-power IoT devices [START_REF] Zandberg | Femto-Containers: DevOps on Microcontrollers with Lightweight Virtualization & Isolation for IoT Software Modules[END_REF]. Last but not least, SUIT allows the ISM to transfer its authority to another entity, e.g., a third-party developer, that can deliver to the ISM some components of a software update (e.g., the executable of the application to be updated) or trigger the update process directly. In this case, the ISM has no mechanism to assess the content of the external software components, and must trust the external entity.

C. PRIVACY-PRESERVING DATA PROCESSING

HArMoNICS includes an access control system that is managed by a dedicated server in the intranet subnetwork (item 3 in Figure 2, in light green). The system secures the access of persons inside the smart building. It also works as the access control system for drivers who want to use the parking lot of the campus. Access control is the process of mediating every request to data and resources owned by a system and determining whether the request should be granted or denied. In general, access control is a necessary condition to build privacy in IoT solutions and to comply with the EU General Data Protection Regulation (GDPR) [START_REF]/679 of the European Parliament (General Data Protection Regulation)[END_REF].

The are several risks associated with such a scenario, the following being the main ones.

• Consent unawareness. This risk relates to a user being unaware of the information disclosed to the system. The user could either provide too much information, e.g., allowing a malicious agent to retrieve her identity, or, on the contrary, inaccurate information, which can lead to wrong decisions or behaviors. • Policy and consent non-compliance. This threat means that, even though the system shows its privacy policies to the users, there is no guarantee that the system actually complies with the advertised policies [START_REF] Deng | A privacy threat analysis framework: supporting the elicitation and fulfillment of privacy requirements[END_REF]. Therefore, although policies claim to prevent it, the user's personal data might still be revealed. • Information disclosure due to wrong design and/or implementation of access control. The information disclosure threats expose personal information to unauthorized individuals [START_REF] Deng | A privacy threat analysis framework: supporting the elicitation and fulfillment of privacy requirements[END_REF]. This can happen in case the access control mechanisms in place are wrongly designed or implemented. Some modern approaches decompose access control in three main components: policy language, model, and enforcement [START_REF] Vimercati | Access control policies and languages[END_REF]. Each of them may carry design/implementation errors. A good privacy-preserving authentication system is an authenticated protocol that does not fully disclose the user identity to a verifier. Only necessary pieces of the user identity (e.g., age, gender, membership etc.) are provided during the verification phase. Furthermore, the authentication sessions should be mutually unlinkable, that is the protocol protects user identity and avoids profiling and tracking of the users.

Another aspect that needs to be taken into consideration within HArMoNICS is how data produced during the use of the II is being handled. The analysis of the usage and transaction logs of the II can provide valuable information on the characteristics and needs of the systems and their users, e.g. services demand, peak hours, and resources sufficiency. However, this type of analysis needs to be performed in a privacy-preserving way, so that the collected data is utilized while remaining protected both from data breaches and unauthorized uses.

Discussion

A promising privacy-enhancing technology that can be used for this purpose is searchable encryption (SE), supporting the storage of usage logs in encrypted form, while data remains available for processing [START_REF] Bösch | A survey of provably secure searchable encryption[END_REF]. This data processing system could be applied to the HArMoNICS smart building, as well as the smart parking lot and vehicle charging services. Desired properties of the SE service include:

• Query expressiveness. Support for complex, multikeyword queries is required, in order to enable deriving useful conclusions from the data analysis.

• Efficiency. The query functionality needs to be efficient, in order to be applicable and practical in a real-world setting such as HArMoNICS. • Dynamic dataset support. Dynamic updates of the encrypted dataset need to be supported in the system, to respond to the dynamic nature of the II. • Multi-client search support. Enabling external entities to perform authorized queries on the encrypted dataset extends the utilization potential and value of the data processing service. Searchable Symmetric Encryption (SSE) is a practical variation of searchable encryption providing balance between efficiency, functionality and security, while supporting the aforementioned requirements [START_REF] Gan | Dynamic searchable symmetric encryption with forward and backward privacy: A survey[END_REF]. An open-source SSE implementation such as Clusion [START_REF]Clusion library[END_REF], based on the IEX SSE scheme [START_REF] Kamara | Boolean searchable symmetric encryption with worst-case sub-linear complexity[END_REF], can be used for the implementation of the HArMoNICS privacy-preserving data processing system.

D. INTRUSION DETECTION

Intrusion detection is one of the main components of a global security strategy. In particular, it is typically considered the second line of defense against attacks. Reasonably, a complex II supported by a large-scale network, made of multiple and heterogeneous devices, is unlikely to be completely secure. Despite all the upstream efforts that are made during the design and development of a critical information system, malicious activities may succeed and compromise the confidentiality, availability, or integrity of the system during its life cycle. An Intrusion Detection System (IDS) aims at detecting such attacks against computer systems and networks. To deal with latent threats, an IDS continuously monitors the running system and analyses the gathered information to detect if an attack occurs or not. When the monitoring mechanism suspects that an attack has occurred (or is in progress), an alert is raised.

The presence of an IDS server within intranet network of HArMoNICS (item 4 in Figure 2, in purple) is useful to allow the investigation of currently trending challenges for the community. In particular, a crucial challenge is related to the availability of an appropriate dataset which is critical in the development of most IDSs. A bulk of state-of-the-art research does not provide reliable performance results since they rely on either the KDD99 or NSL-KDD benchmark datasets, which is concocted of traffic being over 20 years old. In this way, it does not represent recent attack scenarios and traffic behaviors. Obtaining traffic from simulated environments can help overcome this issue when merged with testing more recent datasets, such as the CICIDS 2017 [START_REF] Borah | An enhanced intrusion detection system based on clustering[END_REF]. Published datasets are available for different domains, such as industrial control systems (ICS) [START_REF] Borges Hink | Machine learning for power system disturbance and cyberattack discrimination[END_REF]. HArMoNICS can be used for assessing the effectiveness of datasets against real attack scenarios.

Discussion

An interesting direction for dealing with this scenario is to consider solutions using intrusion models that assume events to belong to a partially ordered set. For each participant of the distributed computation, the input trace describes the sequence of events that occurred locally in the participant's process. An event is a performed action, like sending or receiving a message, but also an internal activity such as a system call. Clearly, for this model to apply, monitoring and logging code must be supported by all the participants, which is often the case.

Based on these traces, each distributed computation can be observed as a partially ordered set of events and be represented by a lattice of consistent cuts. This intermediate representation of learned normal behavior is potentially very large in size. Thus, it is used to infer smaller models that characterize the acceptable sequences of events. These models can take the form of an automaton or a list of temporal properties that have to be satisfied (likely invariants). Several types of models are constructed and used in parallel, as different models are often complementary during the detection phase. Also, using different types of models is a key to reduce false negatives. Furthermore, to reduce false positives during the detection phase, the training phase must consider multiple distinct correct executions: the resulting models are obtained by combining the intermediate models defined during the learning of each normal execution.

E. IOT PROTOCOLS FLAWS

HArMoNICS includes two different scenarios related to the verification of IoT protocols. In the first scenario, the protocol EnOcean [START_REF] Marksteiner | An overview of wireless IoT protocol security in the smart home domain[END_REF], mainly used in smart building domain, has been considered (item 5 in Figure 2, in blue). Briefly, EnOcean is used to implement the communications between IoT devices interacting with a smart HVAC (Heating, Ventilation and Air-Conditioning) system. Since IoT devices are provided by different manufacturers, design flows in the EnOcean protocol may have dramatic effects on the correct behavior of the HVAC system. The HVAC hub server is located in the building area network (or local area network) and communicates through a gateway to the Internet and outside users. Via smartphone or tablet the user can get access to the building network and she can monitor or configure the system. In case of an unusual event the user will be notified immediately. Thus, an attacker could exploit flaws in the EnOcean protocol to carry out the following operations.

• Eavesdropping, i.e. spying on system.

• Replay attack, where (parts) of messages are recorded to use it at a later stage. • Man-in-the-middle attack, where the communication between two communication partners is intercepted, and potentially changed during transmission (modification attack). • Denial-of-Service attack, i.e., preventing legitimate users from accessing the system.

The second scenario, instead, focuses on a risk analysis of two different smart building system configurations through threat modeling. This scenario carries three elements. The first one is modeling a system, e.g., with a threat modeling tool, in order to identify potential threats and vulnerabilities. The second element includes the attack scenario definition through the exploitation of selected vulnerabilities. The last one amounts to a risk analysis of the attack scenarios.

Discussion

Formal verification allows proving the correctness of a target protocol with respect to a certain specification or property with mathematical rigor. Possible checks include verification or falsification of security properties, functional correctness, qualitative and quantitative analysis of protocol specifications or implementations [START_REF] Hofer-Schmitz | Towards formal methods of iot application layer protocols[END_REF] [START_REF] Hofer-Schmitz | Towards formal verification of iot protocols: A review[END_REF], in presence of an attacker.

In the first scenario describe above, the formal verification of EnOcean can be based on ProVerif [START_REF] Blanchet | An efficient cryptographic protocol verifier based on prolog rules[END_REF] [37], i.e., a protocol model checker which considers the well know Dolev-Yao attacker model [START_REF] Dolev | On the security of public key protocols[END_REF]. The first step is the creation of an input model, e.g., based on the protocol specification. Since, in general, model checking the whole protocol specification is computationally expensive, often models include only the most critical parts in the protocol (e.g., initial authentication between the participants) to be verified against the relevant security goals (e.g., authentication happens correctly). Usually, the output of the formal verification process is either a proof of correctness or a potential vulnerability (a.k.a. a counterexample). Since ProVerif also handles unbounded protocol sessions, which are undecidable in general, it may return false positives, i.e., counterexamples/attacks that are not actually executable. For this reason, ProVerif also gives an attack derivation, which helps a human analyst to manually reconstruct an attack.

Instead, the second scenario can be treated via a probabilistic risk analysis of the two system configurations (see above) through model checking [START_REF] Vallant | Threat Modelling and Beyond-Novel Approaches to Cyber Secure the Smart Energy System[END_REF]. Since the problem to be modeled for this scenario is probabilistic, one may consider the Prism model checker [START_REF] Kwiatkowska | Prism: Probabilistic symbolic model checker[END_REF]. Briefly, Prism models are specified through various types of Markov chains, where each transition occurs with a giver probability. Assigned probabilities can correspond to the risk/likelihood score of a certain threat in the threat model.

F. FOG ORCHESTRATION SECURITY

The main idea behind this scenario is to check the placement of Fog and Edge devices and services for possible QoS and security-related issues, and find the non-optimal distribution of services between Fog nodes. Two Fog nodes are physically placed in two different locations and both are connected to the iot network (item 6 in Figure 2, in yellow). These Fog nodes are capable of running communication services to connect with related edge devices. Fog nodes host services that monitor the lighting characteristics in the rooms using light sensors, and are capable to adjust the lighting according to the preferences of the human by activating smart bulbs. Location and presence services are running on the Fog nodes to sense humans in the room and to monitor their exact position. A decision service "knows" the lighting preferences of the particular human, and controls smart bulbs according to the position of that human inside the room. For example, if the human sits on the couch near the TV, the lighting should be dimmed, etc.

The goal of this scenario is to provide a testbed for Fog orchestrators, and for measuring their ability to make decisions on controlling the services according to the QoS and security requirements. Each decision of the orchestrator on starting/stopping/suspending/moving Fog services should be checked for the satisfaction of the minimal requirements imposed by various hardware and software restrictions of the involved physical devices, as well as requirements arising from the specifics of the area of application (e.g., healthrelated data should be protected better than environment monitoring data).

Orchestrators should follow three main steps:

• Each orchestrator should apply requirements on latency, bandwidth, security, and range imposed by the application area and hardware/software capabilities of each Fog node and decide if it is possible to start all required services without violating these requirements; • Orchestrators should find the optimal distribution of the available services between different Fog nodes: this is useful for saving energy and computation resources in cases when some services may be stopped, suspended or moved to another Fog nodes; • Dynamic service allocation should be carried out. Dynamic allocation happens when the situation changes at runtime, and orchestrators must change the distribution of the services between available Fog nodes according to the new conditions.

Discussion

The technique for a Dynamic Service Orchestration, which addresses the issues discussed above, is presented in [START_REF] Morkevicius | Method for dynamic service orchestration in fog computing[END_REF].

The control loop is developed on three main consecutive steps: Monitoring, Optimization, and Execution. Optimization aims to place find which placement of n available services in k Fog nodes makes a set of chosen QoS parameters is optimal. The problem can be solved through a system of inequalities for parameters such that objective functions are minimized. Although, the objective functions are contradicting to each other so there is no single solution to this multi-objective optimization problem that optimizes all the objective functions at the same time.

In fact, the process resolves into two further substeps. Integer Multi Objective Particle Swarm Optimization (IMOPSO) method is used to find a set of Pareto optimal solutions. All service placements in this set are non-dominated (Pareto optimal), which means that each of them is better than all the other ones by at least one criterion. The second step is to choose the best solution from the Pareto optimal set by using the Analytical Hierarchy Process (AHP) [START_REF] Saaty | The seven pillars of the analytic hierarchy process[END_REF]. AHP uses only a pairwise comparison of all alternatives by all objective functions, is easy to implement and gives consistent results.

G. FOG HARDENING

As previously stated, Fog nodes play an important role in the IoT network of HArMoNICS. As a matter of fact, they serve edge computation for end-users in their proximity, sharing the load on the resources provided by cloud servers. However, this network topology optimization exposes the security of the user-and kernel-space software running on Fog nodes, as they directly interact with the end-user device, which may be malicious (item 7 of Figure 2, in orange). Such an exposure poses security risks which threaten the confidentiality of the data processed by user-space Fog applications, the integrity of the kernel-space Fog operating system, and, inherently, of the whole Fog layer of the ZEB.

Attackers leverage memory corruption vulnerabilities to establish primitives for reading from or writing to the address space of a vulnerable application. These primitives form the foundation for code-reuse and data-oriented attacks [START_REF] Szekeres | Sok: Eternal war in memory[END_REF]. The security enhancement should ensure the confidentiality of sensitive data, such as personal user information or user authentication material, that user-space application running on Fog nodes process. Moreover, the security extension should harden the underlying operating system kernel against dataoriented attacks, preventing an attacker from taking over the Fog node, which would allow her to have a foothold in the II network.

Discussion

With respect to the highlighted issues, virtualization extensions of modern CPUs could be leveraged to establish selective memory protection (xMP) primitives [START_REF] Proskurin | xmp: Selective memory protection for kernel and user space[END_REF], that have the capability of thwarting data-oriented attacks. Such extensions, like Intel's Extended Page Table pointer (EPTP), offer the possibility to manage different views on guest-physical memory from inside a VM, without any interaction with a hypervisor. Therefore, selective protection of sensitive data in user or kernel space is obtained by isolating sensitive data in disjoint xMP domains.

In the specific use case scenario, such a solution can be used to harden the user-space decision service that the fog orchestrator deploys on fog nodes, which adjusts the light level based on user preferences received from their end device. Specifically, the end-user data that the service processes and stores in its address space can be isolated in a dedicated xMP domain. This way, the user information is prevented from being leaked in case an attacker exploits a memory corruption vulnerability that may emerge in the decision service.

H. MANAGING PERSONAL DATA IN VEHICLE RECHARGE PROCESS

HArMoNICS includes a vehicle recharge facility. Its main components are the user's personal device, the smart parking lot, and the power distributor infrastructure (item 8 of Figure 2, in dark green). The driver using her personal device initiates the charging process in the smart parking lot. Once the charging process is done, the power distributor (based on the smart meter) sends the charged energy amount to be paid.

The scenario focuses on the payment details and on the related security risks. The payment details may include (i) the driver's name, (ii) bank account and/or credit card information, and (iii) authorization to debit/credit the bank account for the service. The process is as follows: the driver submits her payment details to the parking lot, where the charging is happening. Once done, the parking lot initiates to charge by sending an initiation command to the power distribution infrastructure. Then, the infrastructure charges the car, sends information about the charged energy amount for the payment. Also, the power distribution infrastructure informs the parking lot that the charge is completed. After the parking lot sends the payment details to the smart building, the central management allows performing the payment transaction for the charged energy amount. Then, the lot is informed about the success of the payment and it sends the payment transaction receipt to the user's personal device.

A security issue related to the above scenario is that it is not clear how the driver's personal data, i.e., payment details, are handled during the transaction and whether the treatment of the personal data respects the principles of the GDPR. Verification tools and methodologies can help when designing and implementing data management processes as the one described above. For instance, the DPO tool [START_REF]Dpo tool -evaluate business process[END_REF] can help to assess how much the described process is compliant with the GDPR and recommend means to achieve this compliance [START_REF] Matulevičius | A method for managing gdpr compliance in business processes[END_REF]. For example, in the scenario above, it is possible to determine that the data owner is the driver, and that her personal data, i.e., the payment details, are processed by the recharging infrastructure. Analysis of the process using the DPO tool results in a list of non-compliances, such as:

• Consent is missing (GDPR [START_REF]/679 of the European Parliament (General Data Protection Regulation)[END_REF], Art. 7)

• Privacy policy is missing (GDPR [START_REF]/679 of the European Parliament (General Data Protection Regulation)[END_REF], Art. 13, 14)

• No security measures are present (GDPR [START_REF]/679 of the European Parliament (General Data Protection Regulation)[END_REF], Art. 25)

• Processing task is not being recorded (GDPR [START_REF]/679 of the European Parliament (General Data Protection Regulation)[END_REF], Art. 30)

Discussion

The various non-compliances with regulations can be resolved through the adoption of several measures. For instance, to solve the issue of consent, the driver must provide consent for processing payment details to the infrastructure, and the infrastructure keeps consent for them. If it is not valid, the infrastructure informs the driver about the invalid consent; otherwise, it proceeds with sending the permission to charge the vehicle. The process can be made compliant with security and privacy requirements by adopting TLS protocol to send sensitive personal information. Then, public-key encryption must be applied so that payment details are encrypted before sending to the parking lot. The infrastructure decrypts them before performing the transaction.

Last, a specific task in the process must be allocated after each processing task to log details.

IV. RELATED WORK

HArMoNICS represents a case study that collects, within a single infrastructure, technologies that are related to some major security concerns in real environments. In fact, our proposal integrates both emulated technologies and real components, that replicate some attack vectors of interest. Furthermore, the assets of HArMoNICS are grouped within a virtual machine, open and downloadable by the community. For all these reasons, we believe HArMoNICS to be a distinguished and useful asset for the security community.

Although HArMoNICS is not meant to be a digital twin (DT) framework, it has a few similarities with this kind of systems. Briefly, according to [START_REF] Bolton | The Gemini principles: Guiding values for the national digital twin and information management framework[END_REF] [48] and [START_REF] Catapult | Feasibility of an immersive digital twin: The definition of a digital twin and discussions around the benefit of immersion[END_REF], a DT is a digital replica of a real infrastructure, whose simulated execution is capable of generating the same amount of information as the original system [START_REF] Grieves | Digital twin: Mitigating unpredictable, undesirable emergent behavior in complex systems[END_REF]. In this respect, some of the scenarios of HArMoNICS can be seen as DTs of real systems. However, HArMoNICS is not designed to be generic and reconfigurable, but only for being extended with new scenarios.

Among the existing digital twins and security testbeds, EPICTWIN [START_REF] Kandasamy | EPICTWIN: An Electric Power Digital Twin for Cyber Security Testing, Research and Education[END_REF] is a major proposal focusing on smart grids, where the users can deploy real-world attacks and countermeasures. It includes SCADA workstations, PLCs, end devices, and smart meters executed through a combination of simulation/emulation technologies, including VMs and Matlab-Simulink real-time models. Intuitively, even if EPICTWIN is not an alternative to our proposal, it may be used to implement an infrastructure similar to that of HArMoNICS. To the best of our knowledge, such an implementation does not exist. Furthermore, DTs based on EPICTWIN can be composed with HArMoNICS through the technologies discussed in Section II. Beyond EPICTWIN, the reasoning discussed above also applies to other testbeds based on smart grids. Among them, some prominent examples are PRIME [START_REF] Becejac | PRIME: a real-time cyber-physical systems testbed: from wide-area monitoring, protection, and control prototyping to operator training and beyond[END_REF], the National SCADA testbed [START_REF] Barnes | National SCADA test bed substation automation evaluation report[END_REF], and the infrastructure by the Mississippi State University SCADA Security Laboratory [START_REF] Morris | A control system testbed to validate critical infrastructure protection concepts[END_REF].

Some other authors have proposed systems for assessing smart infrastructures from a mainly functional point of view. As a consequence, security aspects are often neglected. Remarkably, [START_REF] Lu | Developing a digital twin at building and city levels: Case study of West Cambridge campus[END_REF] puts forward a demonstrator staged in a Campus of the West Cambridge university, which resembles the context of HArMoNICS. The work presents a detailed taxonomy for the layers on which an intelligent civil infrastructure must be based, sided by a data systematization model. Another example is [START_REF] Ford | Smart cities with digital twin systems for disaster management[END_REF], where a reference architecture for smart cities, also including a framework for responding to disastrous incidents, is given. Similar reference architectures are given in [START_REF] Dutta | IoT-fog-cloud based architecture for smart city: Prototype of a smart building[END_REF], [START_REF] Alsuhli | A Fog-based IoT Platform for Smart Buildings[END_REF], and [START_REF] Chevallier | A Reference Architecture for Smart Building Digital Twin[END_REF]. Since they have a different target, none of these systems puts emphasis on IT security aspects and, thus, they cannot be directly compared with our work. In fact, they might even be composed with HArMoNICS to build larger case studies.

Finally, from the point of view of the formalization of security issues, [START_REF] Ciholas | The security of smart buildings: a systematic literature review[END_REF] and [START_REF] Laufs | Security and the smart city: A systematic review[END_REF] propose a systematic literature VOLUME x, xxxx review on smart buildings and cities, respectively. Although these works do not provide an implementation, the security concerns gathered there partially overlap with those of HArMoNICS. Again, other security scenarios presented in these works can be integrated with HArMoNICS when implemented.

V. CONCLUSION

In this paper, we presented HArMoNICS, an open-source case study based on a virtual replica of a real intelligent infrastructure located in the Savona Campus of the University of Genoa. HArMoNICS provides a series of vertical scenarios related to major security concerns of intelligent infrastructures, e.g., software integrity and upgradeability, privacy-preserving computing, and intrusion detection. The main goal of HArMoNICS is to become a strategic resource for the security community, which can rely on it for setting up experiments and benchmark activities. The infrastructure is currently used as an environment for the demonstration of security techniques (e.g., see [START_REF] Malina | Post-Quantum Era Privacy Protection for Intelligent Infrastructures[END_REF]) developed in the context of the High-Assurance Intelligent Infrastructure Toolkit program of EU-funded project SPARTA.

In future work, we plan to leverage HArMoNICS for assessing the effectiveness of new methodologies aimed at increasing the security level of the intelligent infrastructures. Moreover, we will consider further security scenarios to enrich HArMoNICS.

FIGURE 1 .

 1 FIGURE 1. The Savona Campus and the Zero-Emission Building (in red).

VOLUME x, xxxx 3

 3 This article has been accepted for publication in IEEE Access. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/ACCESS.2022.3218412 This work is licensed under a Creative Commons Attribution 4.0 License. For more information, see https://creativecommons.org/licenses/by/4.0/

FIGURE 2 .

 2 FIGURE 2. HArMoNICS network infrastructure overview.

FIGURE 3 .

 3 FIGURE 3. Scenario implementation overview.

  This article has been accepted for publication in IEEE Access. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/ACCESS.2022.3218412 This work is licensed under a Creative Commons Attribution 4.0 License. For more information, see https://creativecommons.org/licenses/by/4.0/ ory safety capabilities (such as strong typing, present in other modern languages) enables attackers to exploit these flaws by maliciously altering the program behavior by partially or entirely hijacking control-flow.

VOLUME x, xxxx 5

 5 This article has been accepted for publication in IEEE Access. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/ACCESS.2022.3218412 This work is licensed under a Creative Commons Attribution 4.0 License. For more information, see https://creativecommons.org/licenses/by/4.0/

VOLUME x, xxxx 7

 7 This article has been accepted for publication in IEEE Access. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/ACCESS.2022.3218412 This work is licensed under a Creative Commons Attribution 4.0 License. For more information, see https://creativecommons.org/licenses/by/4.0/

VOLUME x, xxxxThis article has been accepted for publication in IEEE Access. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/ACCESS.2022.3218412 This work is licensed under a Creative Commons Attribution 4.0 License. For more information, see https://creativecommons.org/licenses/by/4.0/ Roascio et al.: HArMoNICS: High-Assurance Microgrid Network Infrastructure Case Study

VOLUME x, xxxxThis article has been accepted for publication in IEEE Access. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/ACCESS.2022.3218412 This work is licensed under a Creative Commons Attribution 4.0 License. For more information, see https://creativecommons.org/licenses/by/4.0/ Roascio et al.: HArMoNICS: High-Assurance Microgrid Network Infrastructure Case Study

VOLUME x, xxxxThis article has been accepted for publication in IEEE Access. This is the author's version which has not been fully edited and content may change prior to final publication. Citation information: DOI 10.1109/ACCESS.2022.3218412 This work is licensed under a Creative Commons Attribution 4.0 License. For more information, see https://creativecommons.org/licenses/by/4.0/

This work is licensed under a Creative Commons Attribution 4.0 License. For more information, see https://creativecommons.org/licenses/by/4.0/

VOLUME x, xxxx

VI. ACKNOWLEDGMENTS

Heartfelt thanks go to all colleagues not included in the list of authors but decisive for the activity: Katharina Hofer-Schmitz (Joanneum Research, Austria), Manon Knockaert, Jean-Marc Van Gyseghem (University of Namur, Belgium), Petr Dzurenda (Brno University of Technology, Czech Republic), Tewodros Beyene (Fortiss Research Institute, Germany), Mari Seeba, Jake Tom (University of Tartu, Estonia), Joaquin Garcia-Alfaro, Jean-Max Dutertre, Jean-Luc Danger, Maryline Laurent (Mines-Télécom Institute, France), Michel Hurfin, Ludovic Mé (National Institute for Research in Computer Science and Automation, France), Paolo Prinetto, Alessandro Armando (National Interuniversity Consortium for Informatics, Italy), Giorgio Bernardinetti, Francesco Mancini, Gabriele Restuccia (National Consortium for Telecommunications, Italy), Uwe Roth, Qiang Tang (Luxembourg Institute of Science and Technology), Marek Pawlicki (ITTI Institute, Poland).

This paper is supported by European Union's Horizon 2020 research and innovation programme under grant agreement No. 830892, project SPARTA.


Leila Amgoud
email: amgoud@irit.fr

Florence Dupin De Saint-Cyr

A Semantics for Agent Communication Languages based on commitments and penalties

Keywords: Agent Communication Languages, Commitment, Penalties

In complex multi agent systems, the agents may be heterogeneous and possibly designed by different programmers. Thus, the importance of defining a standard framework for agent communication languages (ACL) with a clear semantics has been widely recognized. The semantics should meet two important objectives: verifiability and flexibility. Classical proposals (mentalistic semantics and social semantics) fail to meet these objectives.

. This makes it more general than the existing ones.

Introduction

When building multi-agent systems, we take for granted the fact that the agents which make up the system will need to communicate and to engage in the different types of dialogue identified by Walton and Krabbe in [START_REF] Walton | Commitment in Dialogue: Basic Concepts of Interpersonal Reasoning[END_REF], using a communication language (ACL). The definition of an ACL from the syntactic point of view (the different speech acts 1 that agents can perform during a dialogue) poses no problems. The situation is different when semantics is taken into account. Any communication language must have a well-defined semantics. Given that agents in a multi-agent system may be independently designed by different programmers, a clear understanding of semantics is essential. Moreover, the semantics should meet two important properties: verifiability and flexibility. Although a number of agent communication languages have been developed, obtaining a suitable formal semantics for ACLs which satisfies the above objectives remains one of the greatest challenges of multi-agent theory. There are mainly two categories of semantics: the mentalistics semantics and the social ones. The mentalistic semantics, used in KQML [START_REF] Finin | Kqml as an agent communication language[END_REF] and FIPA [START_REF] Fipa | Agent communication language[END_REF], is based on a notion of speech act close to the concept of illocutionary act as developed in speech act theory [START_REF] Austin | How to do things with words[END_REF][START_REF] Searle | Foundations of illocutionary logic[END_REF]. The basic idea behind this semantics is to define the conditions under which a given speech act can be played. Unfortunately, the conditions are based on the mental states of the agents and this makes the semantics not verifiable since one cannot access to those mental states to check whether the conditions are really satisfied or not. Consequently, such category of approaches violates one of the important properties of a semantics.

In the second category of semantics, called social and developed in [START_REF] Colombetti | A commitment-based approach to agent speech acts and conversations[END_REF][START_REF] Singh | Agent communication languages: Rethinking the principles[END_REF][START_REF] Singh | A social semantics for agent communication languages[END_REF], primacy is given to the interactions among the agents. The semantics is based on social commitments brought about by performing a speech act. For example, by affirming a data, the agent commits on the truth of that data. After a promise, the agent is committed carrying it out. There are several weak points of this approach and the most relevant one is the fact that the concept of commitment itself is ambiguous and its semantics is not clear. According to the performative act, the semantics of the commitment differs. (See section 5 for more details) Another limitation of both approaches is the fact that they are neither modular nor general. Since they are defined on particular speech acts, if a new speech act is needed for a particular dialogue, then the semantics should be extended.

Our aim is to define a semantics which prevents the shortcomings of the existing approaches while keeping their benefits. Thus, we propose a semantics which satisfies the two main properties. Our approach is social in nature since it is based on the notion of commitments. An agent may have two kinds of commitments:

1. The commitments made by the agent itself during the dialogue such as promises and that it should respect. Such commitments allow the evaluation of the degree of honesty of the agent. Indeed, an agent which respects its commitments is said honest. 2. The commitments for replying to requests made by the other agents. For instance if the agent receives a question from another agent, then it should answer. Such commitments ensures the cooperativity of the agent.

From a syntactic point of view, these commitments are modelled via a notion of commitment store as originally defined by MacKenzie in [START_REF] Mackenzie | Question-begging in non-cumulative systems[END_REF]. Indeed, each agent is supposed to be equipped with a commitment store which will keep track of the different commitments of the agent. These stores are accessible for all the agents.

The semantics of a commitment is unique and is given by the sanction, called penalty, associated to a commitment in case it is not respected by the agent.

Another interesting feature of our semantics is the fact that it is defined on the well-known categories of speech acts defined by Searle in [START_REF] Searle | Speech acts[END_REF][START_REF] Searle | Foundations of illocutionary logic[END_REF]. Indeed, Searle has defined five categories of performatives: the assertives, the directives, the commissives and finally the expressives. We will show that we can define a semantics for each category without worrying about the different speech acts it may contain. This makes our semantics flexible and more general than the existing ones.

The proposed semantics is also verifiable since the penalty associated to a move is computed directly from its category and the agent commitment store which is visible to all agents; so there is no need to know what the agent really believes, only the category of the moves and previous moves are taken into account.

The paper is organized as follows: Section 2 introduces the logical language that will be used throughout the paper. In section 3 we present the basic concepts of our semantics. In particular, we define the two kinds of commitments of an agents as well as the two corresponding penalties. In section 4, we define the semantics of the four categories of speech acts defined by Searle (we do not consider the expressive category). Section 5 compares our approach to existing semantics and finally, section 6 concludes with some remarks and perspectives.

Background

In this section we start by presenting the logical language which will be used throughout this paper. We will distinguish among action variables (AV) and non-actions variables (N AV). AV and N AV are supposed to be disjoint (i.e. AV ∩ N AV = ∅).

L will denote a propositional language built from AV ∪ N AV. denotes classical inference and ≡ denotes logical equivalence.

Arg(L) will denote the set of all the arguments that can be constructed from L. An argument is a pair (Γ, φ) where Γ is a set of formulas of L, called the support of the argument and φ ∈ L is its conclusion. In [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF], Dung has presented a powerful argumentation framework which takes as input a set of arguments and the different conflicts which may exist between them, and returns among all the arguments the "good" ones, called the acceptable arguments.

Let A = {a 1 , . . . , a n } denote the set of agents. A communication language is based on a set of speech acts. In what follows, S denotes the set of speech acts of a given communication language. In [START_REF] Amgoud | An argumentation-based semantics for agent communication languages[END_REF], a communication language has been defined using the following set of speech acts: {Question, Challenge, Assert, Accept, Ref use, Request, P romise, Retract, Argue }. Assert allows the exchange of information such as "the weather is beautiful" and "It is my intention to hang a picture". Request is invoked when an agent cannot, or prefer not to, achieve its intentions alone. The proposition requested differs from an asserted proposition in that it cannot be proved true or false. The decision on whether to accept it or not hinges upon the relation it has to the agent's intentions. An agent will make a P romise when it needs to request something from another, and has something it doesn't need which can offer in return. In replying to an assertion, a request or a promise, an agent can accept, refuse or ask a question such as "is it the case that p is true ?". Another kind of question is called a challenge. It allows an agent to ask another agent why it has asserted a proposition or requested something, for example "why newspapers can't publish the information X?". The answer to a challenge should be an argument. Argue allows agents to exchange arguments, and Retract allows them to retract propositions previously asserted or requested.

In [START_REF] Searle | Speech acts[END_REF][START_REF] Searle | Foundations of illocutionary logic[END_REF], Searle has identified five categories of speech acts according to what he calls their illocutionary purpose, their psychological direction to the world, their expressed state, and their propositional content. The five categories are as follows:

Assertive speech acts: The speaker claims that some proposition is true. This category contains speech acts like "inform" or "assert". For instance, Inform: the sky is blue or Inform: it is my intention to hang a mirror. In what follows, we will refer to the set of all speech acts of this category by S 1 . Directive speech acts: The speaker attempts to get the hearer to do something. This category includes speech acts like "Request", "Question" and "Challenge". For instance, Request: clean your room!, Question: is p true. In what follows, we will refer to the set of all speech acts of this category by S 2 . Commissive speech acts: The speaker commits to some future course of action. An example of a commissive speech act is "promise", for instance Promise: I will do it. In what follows, we will refer to the set of all speech acts of this category by S 3 . Expressive speech acts: The speaker expresses some psychological state. For instance, an agent can say Im sorry. Declarative speech acts: The speaker brings about a different state of the world. For instance, "Propose", "Accept", "Refuse", "Retract" are declaratives. In what follows, we will refer to the set of all speech acts of this category by S 4 .

In this paper, we are more concerned with setting a semantics for dialogues between artificial agents. Thus, the category of expressive speech acts will not be considered here.

S 1 , S 2 , S 3 , S 4 is seen as a partition of the set S of speech acts. This means that ∀i, j ∈ [START_REF] Amgoud | Modelling dialogues using argumentation[END_REF][START_REF] Austin | How to do things with words[END_REF], i = j ⇒ S i ∩ S j = ∅ and S 1 ∪ S 2 ∪ S 3 ∪ S 4 = S. Hence, every speech act symbol belongs to one and only one of the four categories S 1 or S 2 or S 3 or S 4 .

Definition 1 A move is a formula a : x where a ∈ S is a speech act and x is either a propositional formula (x ∈ L) or an argument (x ∈ Arg(L)). Let M be the set of moves.

For instance, Question : sky blue is a move meaning that the agent asks whether the sky is blue or not. Here, "Question" is a speech act and sky blue is a propositional formula (whose value is true or false).

semantics

Commitment

In the scientific literature, one can find proposals where the semantics of an ACL is defined in terms of commitments. Examples of these are given by Colombetti [START_REF] Colombetti | A commitment-based approach to agent speech acts and conversations[END_REF] and Singh [START_REF] Singh | Agent communication languages: Rethinking the principles[END_REF][START_REF] Singh | A social semantics for agent communication languages[END_REF]. The authors argued that agents are social entities, involved in social interactions, then they are committed to what they say.

In recent years, it has been argued that informal logic has much to offer to the analysis of inter-agent communication. Central in these approaches are the notions of dialogue games and (social) commitments. One rather influential dialogue game is DC, proposed by MacKenzie [START_REF] Mackenzie | Question-begging in non-cumulative systems[END_REF] in the course of analysing the fallacy of question-begging. DC provides a set of rules for arguing about the truth of a proposition. Each player has the goal of convincing the other, and can assert or retract facts, challenge the other player's assertions, ask whether something is true or not, and demand that inconsistencies be resolved. Associated with each player is a commitment store, which holds the commitments of the players during the dialogue. Commitments here are the information given by the players during the dialogue. There are then rules which define how the commitment stores are updated. Take for instance the assertion, it puts a propositional statement in the speaker's commitment store. What this basically means is that, when challenged, the speaker will have to justify his claim. But this does not presuppose that the challenge will come at the next turn in the dialogue.

For our purpose, we adopt this presentation of commitments. In this paper we are not interested in modeling the agent's reasoning, we only consider what is said by each agent. Our purpose is to provide a semantics for the dialogue without worrying about the mental states of the agents. Each agent is supposed to be equipped with a commitment store, accessible to all agents, which will contain its commitments made during the dialogue. The union of the commitment stores of all agents at turn t can be viewed as the state of the dialogue at turn t. We adopt a commitment store much more structured than the one presented in previous works on dialogue [START_REF] Amgoud | Modelling dialogues using argumentation[END_REF][START_REF] Amgoud | Arguments, dialogue, and negotiation[END_REF]. It keeps tracks of two kinds of commitments:

-The commitments made in the dialogue by the agent itself such as assertions and promises. -The commitments made by other agents, such as requests, challenges and questions. For instance if an agent a i makes a request r to another agent a j , the request (r) is stored in the commitment store of a j . Hence, a j is said committed to satisfy this request.

More formally, for each agent a i , we denote CS i its commitment store, containing statements and issues to be resolved.

Definition 2 A commitment store CS i associated to an agent a i is a pair:

CS i = A i , O i
where The disctinction between the two kinds of commitments is necessary because statements expressed by the agent itself commit its honesty whereas statements expressed by other agents commit its cooperativity. They are the different by nature and, in our opinion, should not be mixed. From the above definition, it is also clear that assertive, commissive and declarative speech acts are related to the first kind of commitments (honesty), whereas directive speech acts are related to the second kind of commitments.

-A i ⊆ M

Penalties

Each time an agent makes a speech act, it makes a commitment. So, it is natural to associate to each commitment a penalty which sanctions the agent if it does not respect this commitment. For the sake of simplicity, we consider that the cost associated to a move depends only of its category.

Definition 3 (Penalty) Let α 1 , α 2 , α 3 and α 4 be numbers in [0, +∞] associated respectively to the categories S 1 , S 2 , S 3 and S 4 .

A penalty associated with a category S i is the number α i .

We distinguish between two kinds of bad behaviors: i) to not be honest, and ii) to not cooperate. Hence, to each commitment store a pair of costs is defined. Formally, the cost associated to the commitment store CS i = A i , O i of agent a i at time t, is a pair c(A i ), c(O i ) , where c(A i ) is the cost associated to the statements of agent a i which are violated, and c(O i ) is the cost associated to the requests made by other agents and to which agent a i has not answered yet. These costs are computed by summing penalties of moves. Deciding which moves are to take into account depends on their categories.

With such a semantics for an agent communication language, a "rational" protocol should be defined in such a way that each agent aims to minimize the costs associated to its commitment store. This notion of protocol is beyond the scope of this paper.

The semantics of the categories of speech acts

In this section we will examine how the penalty associated to a move of each category can be computed, i.e., we will describe when a given commitment is violated by the agent.

4.1 Categories: Assertives (S 1 ) and Declaratives (S 4 )

The assertives and the declaratives behave exactly in the same way, but apply on two distinct languages. Indeed, for the assertives, the content of the moves are formulas of L built only on the set of non-action variable (N AV), whereas the ones of declaratives are built on action variables (AV). During a dialogue, an agent may claim that some statement is true. This agent is then, not allowed to contradict itself during all the dialogue otherwise it should pay a penalty.

Storage All the assertive moves are stocked in the commitment store of the agent, exactly in the part A i . When an assertive move comes as a response to a question or a challenge, for instance, this question or challenge is removed from the set O i . However, if it is rather a response to a kind of commissive speech act like a promise, then the promise is removed from A i . ∀a ∈ S 1 , there are two cases, either the associated assertion is a formula or it is an argument:

-∀x ∈ L, if agent a i commits a : x then

• a : x is added to A i , and • ∀(a : y) ∈ O i , such that a ∈ S 2 and y ∈ L and x y, a : y is removed from O i , and • ∀(a : y) ∈ A i , such that a ∈ S 3 and y ∈ L and x y, a : y is removed

from A i . -∀x = Γ, ϕ ∈ Arg(L), if agent a i commits a : x then • a : x is added to A i ,

and

• ∀(a : y) ∈ O i , such that a ∈ S 2 and y ∈ L and ϕ y, a : y is removed from O i , and • ∀(a : y) ∈ A i , such that a ∈ S 3 and y ∈ L and ϕ y, a : y is removed from A i Associated Cost: Costs associated to assertives concern non-honesty. An assertive move a : x, where a ∈ S 1 and x ∈ L ∪ Arg(L), is a violated commitment if the part A i of agent a i 's commitments store allows to deduce that the formula x is false or to deduce that one formula of the support of the argument x is false. Hence, the cost associated to an assertive is given by: ∀(a : x) ∈ A i , if a ∈ S 1 , there are two cases, either the assertion x is a formula or it is an argument:

-∀x ∈ L, c(a : x) = α 1 if A i ¬x, 0 otherwise -∀x = Γ, ϕ ∈ Arg(L), c(a : x) = α 1 if ∃ϕ Γ, A i ¬ϕ, 0 otherwise 4.2 Category S 2 : Directives
The agent attempts to get another agent to do something. For instance, Request, Question, Challenge are Directives.

Storage Directives of Agent a i towards Agent a j are stored in the part O j of the commitment store of agent a j , if there is not already an answer to it in A j (which can be either assertive or declarative): ∀a ∈ S 2 , the directive a : x of Agent a i towards Agent a j is added to O j if ∃(a : y) ∈ A j , such that a ∈ S 1 ∪ S 4 and:

y ∈ L and y x or y = Γ, ϕ ∈ Arg(L) and ϕ y.

Associated Cost Costs associated to directives are only penalties of noncooperativity. It means that a directive is violated if it is in the part O i of Agent a i (agent a i has not already answered to it).

∀(a : x) ∈ O i if a ∈ S 2 , ∀x ∈ L, c(a : x) = α 2

Category S 3 : Commissives

The agent commits to some future course of action. For instance, Promise is in the Commissives. The most general form of promise is "if ϕ is true then I swear that ψ will be true", "if you do that, I will kill you". It can be encoded by the move P romise : ϕ → ψ.

Storage Commissives of Agent a i are stored in the part A i of its commitment store if the associated formula is not already true in A i (either because there is an assertive or a declarative move which makes it true): ∀a ∈ S 3 , the commissive a : x of Agent a i is added to A i if ∃(a : y) ∈ A i , such that a ∈ S 1 ∪ S 4 and:

y ∈ L and y x or y = Γ, ϕ ∈ Arg(L) and ϕ y.

Associated Cost Costs associated to commissives are only costs of non-honesty. As long as a commissive is in the commitment store, it costs a penalty since it means that this commissive has not been made.

∀(a : x) ∈ A i If a ∈ S 3 , ∀x ∈ L, c(a : x) = α 3

Summary

To sum up, the penalties associated to a commitment store CS i of an agent a i at turn t are: cooperation penalty:

p c (CS i = (a:x)∈Oi α 2
honesty penalty: The first standard agent communication language is KQML [START_REF] Finin | Kqml as an agent communication language[END_REF]. It has been developed within the Knowledge Sharing Effort, a vast research program funded by DARPA (the US Defense Advanced Research Projects Agency). More recently, the Foundation for Intelligent Physical Agents (FIPA) has proposed a new standard, named ACL [START_REF] Fipa | Agent communication language[END_REF]. Both KQML and ACL have been given a mentalistics semantics. The semantics is based on a notion of speech act close to the concept of illocutionary act as developed in speech act theory [START_REF] Austin | How to do things with words[END_REF][START_REF] Searle | Foundations of illocutionary logic[END_REF]. Such semantics assumes, more or less explicitly, some underlying hypothesis in particular, that the agents are sincere and cooperative. While this may be well fitted for some special cases of interactions, it is obvious that some dialogue types listed by Walton and Krabbe in [START_REF] Walton | Commitment in Dialogue: Basic Concepts of Interpersonal Reasoning[END_REF] are not cooperative. For example, assuming sincerity and cooperativity in negotiation may lead to poor negotiators. Another more important limitation of this approach is the fact that it is not verifiable since it is based on the mental states of the agents. Our semantics does not refer at all to the mental states of the agents. Moreover, it does not treat particular speech acts as it is the case with this mentalistic approach.

p h (CS i ) =
In the second approach, called social and developed in [START_REF] Colombetti | A commitment-based approach to agent speech acts and conversations[END_REF][START_REF] Singh | Agent communication languages: Rethinking the principles[END_REF][START_REF] Singh | A social semantics for agent communication languages[END_REF], primacy is given to the interactions among the agents. The semantics is based on social commitments brought about by performing a speech act. For example, by affirming a data, the agent commits on the truth of that data. After a promise, the agent is committed carrying it out. There are several weak points of this approach and we summarize them in the three following points: 1. The definition of commitments complicates the agent architecture in the sense that it needs an ad hoc apparatus. The commitments are introduced especially for modeling communication. Thus agents should reason not only on their beliefs, etc but also on the commitments. In our approach, we didn't introduce any new language to treat commitments. We call a commitment any information stocked in a commitment store. Handling these commitments (to add a new commitment, to retract a commitment, to achieve a commitment, to violate a commitment) is done directly on the commitment store. 2. The level at which communication is treated is very abstract, and there is a considerable gap to fill in order to bring the model down to the level of implementation. However, the semantics presented in this paper can be implemented easily.

3. The concept of commitment is ambiguous and its semantics is not clear. According to the speech act, the semantics of the commitment differs. For example:

Inform: by affirming a data, the agent commits on the truth of that data. The meaning of the commitment here is not clear. It may be that the agent can justify the data or can defend it against any attack, or the agent is sincere. Request: According to Colombetti [START_REF] Colombetti | A commitment-based approach to agent speech acts and conversations[END_REF] after a request, the receiver precommits to carry it out. This idea is in our opinion drawn from the notion of protocol. The protocol specifies for each act the set of allowed replies. So after a request, generally the receiver can accept it, reject it or propose another alternative.

The last approach developed by Pitt and Mandani in [START_REF] Pitt | A protocol based semantics for an agent communication language[END_REF] is based on the notion of protocol. A protocol defines what sequences of moves are conventionally expected in the dialogue. The meaning of a speech act then equates with the set of the possible following answers. However, protocols are often technically finite state machines. This turns out to be too rigid in several circumstances. Current research aims at defining flexible protocols, which rely more on the state of the dialogue, and less on dialogue history. This state of dialogue is captured through the notion of commitment.

Conclusion

This paper has introduced a general semantics of any agent communication language. The semantics is general in the sense that it can be used with any set of speech acts since it is defined on categories of speech acts rather than the speech acts themselves. Indeed, for the first time, we have a semantics of an ACL which is defined independently from the syntax of that ACL. This makes the semantics flexible and general. The new semantics is social in nature and is based on the notion of commitments. However, our modeling of this notion is very different from the existing approaches. Indeed, the commitments are modeled as in MacKenzie's system DC [START_REF] Mackenzie | Question-begging in non-cumulative systems[END_REF]. A commitment is any information stocked in the commitment store of the agent. Two kinds of commitments have been distinguished: the commitments to satisfy or to respect what the agent has already said, promised, etc. and the commitments to answer to other agents. Unlike in the existing approaches, the semantics of a commitment is unique and is given via the notion of penalty that should be paid if an agent does not respect that commitment. Our semantics goes somewhat beyond the existing approaches in giving an operational, verifiable and flexible semantics. An extension of this work would be to simplify the protocols by extending our semantics by rules which were generally defined in the protocol itself. For instance, in the semantics, we can sanction agents which repeat, the same move several times during a dialogue. Another extension would be to refine the penalties by introducing granularity in the categories of speech acts. The idea is, maybe, to associate different penalties for the speech acts in order to capture the idea that some commitments are harder to violate than others. The same idea applies also to the content of the moves.

( 3

 3 a:x)∈Ai s.t. a∈S1(resp.S4) and x= Γ,ϕ ∈Arg(L) and ∃ψ∈Γ s.t. Ai ¬ψ α 1 (resp.α 4 ) + (a:x)∈Ai s.t. a∈S1(resp.S4) and x∈L and Ai ¬x α 1 (resp.α 4 ) + (a:x)∈Ai s.t. a∈S3 α Or equivalently, (since we suppose that c(a : x) only depends on the category of a): p c (CS i ) = (a:x)∈Oi,a∈S2 c(a : x) and p h (CS i ) = . a ∈ S 1 ∪ S 4 and or x = Γ, ϕ ∈ Arg(L) and ∃ψ ∈ Γ s.t. A i ¬ψ x ∈ L and A i ¬x s.t. a ∈ S 3 c(a : x)

  stands for the set of moves of agent a i whose speech acts are in {S 1 , S 3 , S 4 }.-O i ⊆ M stands for the set of moves received by agent a i and whose speech acts are in S 2 .

The speech acts are also called elsewhere illocutionary acts or performatives.