The widespread presence of cyber-physical systems necessitates a reliable assurance mechanism for audit logging across various discrete and continuous components of these systems. This paper explores an implementation model for cyber-physical systems. We introduce an algorithm designed to equip such systems in accordance with a formal specification of audit logging requirements, which provably ensures the generation of accurate audit logs in any instrumented system. The accuracy of the audit log is studied within an informationalgebraic semantic framework of audit logging.
Audit logs play a crucial role in enhancing security across various domains by providing a detailed
record of system activities and events. They serve as an indispensable source of information for
detecting and investigating security incidents, breaches, and unauthorized access attempts [
In cyber-physical systems (CPSs), where the integration of physical processes with computing and networking capabilities is prevalent, audit logging becomes even more critical. These systems are subject to various security threats, including cyber attacks targeting critical infrastructure [2], industrial control systems [3] and autonomous vehicles (AVs) [4]. Audit logging in CPSs enables the tracking of interactions between physical and digital components, which provides insights into system behavior, anomalies, and potential vulnerabilities. For instance, in smart grid systems, audit logs can help detect and prevent unauthorized access to energy distribution networks, ensuring the reliability and integrity of the grid [5]. Similarly, in AVs, audit logs are essential for recording sensor data, decision-making processes, and helping with the forensic analysis and liability attribution in case of accidents or cyber attacks [6].
In recent years, information-algebraic models [7], have emerged as valuable semantic frameworks for audit logging. These models interpret audit logs and the runtime structure of processes as elements that reside in an information algebra, providing intuitive insights into their information content. The reliability of audit logging hinges on this interpretation, which compares the information content of audit logs with that of the program at runtime. Leveraging this framework, an implementation model has been proposed for linear [8] and concurrent [9] computations, ensuring accurate audit logging through instrumentation techniques.
In this paper, we explore the application of the aforementioned information-algebraic framework in CPSs. To this end, we use a programming-linguistic model of CPSs, known as hybrid programs (HPs) [10, 11, 12]. Hybridity in the context of HPs refers to the simultaneous presence of discrete computational elements and continuous physical dynamics inherent in CPSs. HPs serve as a fundamental programming language for CPSs, allowing for the specification of integrated discrete and continuous behaviors. We use a variant of HPs, where the semantics is specified operationally (rather than denotationally) to facilitate the specification of audit log generation at runtime. Our formalism provides a model for developing CPS tools with correctness guarantees. This language model ofers the following features: i) The language model supports the hybrid nature of CPSs, accommodating both discrete computational steps and continuous physical behavior. ii) Leveraging a variant of HPs, our approach benefits from concise syntax and semantics. This facilitates the description of a broad spectrum of hybrid-dynamic systems. iii) In order to articulate auditing requirements efectively, our model incorporates timestamps as part of the runtime environment. This enables the specification of the ordering of significant events. iv) Fundamental to specifying auditing requirements is the abstraction of secure operations. Named functions serve as these fundamental units. They ofer a versatile tool for expressing auditing needs across diferent languages and systems.
Utilizing the formalism with the aforementioned features empowers us to model CPSs that ensure the accurate generation of audit logs in line with the developed semantic framework. In this paper, we present an instrumentation algorithm designed to modify an HP based on precise audit logging requirements. We demonstrate the correctness of this algorithm, as per the semantic framework, which ensures that the instrumented concurrent system produces accurate audit logs. The implementation of audit logging policies through code instrumentation ofers a separation of policy from code, which lays the groundwork for studying the efectiveness of enforcement mechanisms using formal methods. Additionally, it can be automatically applied to legacy code to bolster system accountability. An Illustrative Example Let’s consider a simplified scenario to illustrate the necessity of studying correct audit logging in CPSs. We will revisit this example multiple times throughout the paper. Our example is an AV system that includes a controller and a physical machinery, and the task is to log a significant event like hard braking. Here is how such a sequence of events might unfold, culminating in a log entry: i) The controller continuously monitors the vehicle’s speed and uses sensors to detect objects in its path. For instance, as the vehicle cruises at 60 mph, a pedestrian unexpectedly steps onto the road. ii) The detection of a pedestrian in the vehicle’s path triggers the controller’s obstacle avoidance algorithm. The controller assesses the distance and speed relative to the obstacle. It calculates that normal braking will not sufice to avoid a collision. iii) Based on the controller’s decision, a command is sent to the physical machinery to execute a hard brake. iv) The physical machinery applies the vehicle’s brakes forcefully and quickly to reduce speed dramatically in a short time. As the hard braking occurs, this critical action is captured as a log event. The system records this event along with pertinent details such as the vehicle’s speed at the time of braking, the time, and the location. Retroactively, the log can be reviewed for compliance with safety protocols or used for improving the decision-making algorithm based on real-world outcomes. In this scenario, the sequence of detection, decision, execution, and logging is crucial for ensuring both the immediate safety of the vehicle’s occupants and others on the road, as well as for long-term improvements and accountability in AV operations.
Paper Outline The rest of the paper is organized as follows: In Section 2, we review the informationalgebraic semantic framework for correct audit logging. In Section 3, we explore the implementation model for HPs by specifying the source and target language models, as well as the instrumentation algorithm that maps an HP from the source language to an HP in the target language. In addition, towards the end of this section the main results of the work are specified. Section 4 discusses the related work. Finally, Section 5 concludes the paper.
In this section, we explore the information-algebraic semantics of audit logging in an informal manner. The content of this section has originally been explored elsewhere formally [8]. We avoid delving into the detailed formal presentation here for the sake of economy of space. 2.1. Information-Algebraic Semantic Framework Audit logs abstract program states into configurations , transitioning via ⟶ ′. A program trace is a sequence of these configurations, with being all such sequences and ( ) their initial segments. A program p or configuration can produce a trace ′, and if ∈ ( ′), we denote this as p ⇓ or ⇓ .
Information algebra is used to define audit log correctness. In Section 2.2, we use this framework to represent specific audit logging criteria. An information algebra (Φ, Ψ) consists of Φ, a semigroup of information elements, and Ψ, a lattice of query domains. It includes combination (⊗) and focusing (⇒) operations that adhere to specific properties governing their interactions. [7]. In the information algebra framework, elements , ∈ Φ are combined using ⊗ , and information is selectively extracted using ⇒ based on the querying domain ∈ Ψ. The combination of information elements introduces a partial order, ≼, where ≼ means that combining and results in , indicating contains all the information of .
is injective and monotonically increasing, indicating that longer traces contain more information than their prefixes.
ent execution models and information formats. Concrete implementations of this specification are detailed in later sections to guide audit logging practices. The logging specification ∶ → Φ describes the information that should be logged for a given execution trace . Note that ⌊⋅⌋ and both map traces to information elements, but serve diferent purposes: ⌊ ⌋ captures all information in a trace, while ( ) specifies what should be logged during that trace’s execution.
An audit log, denoted as , collects data during runtime, with representing the set of all possible logs. To assess a log’s correctness, we compare its content to the trace that produced it, using a mapping ⌊⋅⌋ ∶ → Φ. This mapping must satisfy that larger audit logs contain more information, by ensuring that ⌊ ⌋ ≼ ⌊ ′⌋ for ⊆ ′. An audit log is deemed correct with respect to a logging specification and a program trace if both ⌊ ⌋ ≼ ( ) and ( ) ≼ ⌊ ⌋ are satisfied. The former indicates the necessity of the information in the audit log, while the latter signifies the suficiency of that information.
We define ( ) to extract audit logs from any given program configuration, . This log expands as execution progresses. is used to represent the logs accumulated over a trace. The residual log of a finite program trace is , denoted by ⇝ , if = 0 1 ⋯ and ( ) = .
add required audit logging. The process results in a target program that generates specified logs. to
The instrumentation algorithm should maintain the original program’s semantics while adding programs p and logging specifications
where (p, ) is applicable. audit logging, ensuring the target program behaves similarly to the source, except for logging differences. This concept, called semantics preservation, uses a correspondence relation ∶≈ to link source and target traces, adaptable to various program implementations. The instrumentation algorithm is semantics-preserving if it ensures that for every trace of the original program p, there is a corresponding trace ′ in the instrumented program such that ∶≈ ′, and vice versa. This applies to all
respect to the logging specification and the source trace. This criterion must hold for any source program, any logging specification, and any possible log generated by the instrumented program. 2.2. Instantiation of Logging Specification
mation algebra for practical application. We focus on logical specifications for audit logs, favoring ifrst-order logic (FOL) for its expressive power and compatibility with logic programming engines.
To instantiate information algebra, we need to instantiate the set Φ of information elements, the lattice Ψ of querying domains, and the combination and focusing operators. To this end, we consider as the set of closed sets of FOL formulas, established under a proof-theoretic deductive system.
by considering a query domain as a subset of FOL, defined over specific predicate involves taking the closure of the union of two sets of formulas, and focusing entails taking the closure of the intersection of an information element and a query domain.
( ), where ∈
is a subset of predicate symbols. Finally, combination mapping interprets both execution traces and audit logs as information elements.
) as a framework for audit logging, we also need to instantiate the maption. Then, to interpret both traces and logs as information elements in (Φ , Ψ ), we instantiate ∪ ) → (
) as an injective and monotonically increasing funcspecification (Γ, ) ∶ → Φ is defined as (Γ, ) = ↦ (⌊ ⌋ ⊗ We define a logging specification
using a set of FOL rules Γ and a set of specific predicate symbols . This specification maps a trace to predicates in derivable from Γ and events in , i.e., a logging (Γ))⇒ ( ). Φ
We define ping ⌊⋅⌋. This ⌊⋅⌋ = 3. Implementation Model on Cyber-Physical Systems This section introduces an implementation model aimed at ensuring accurate audit logging in CPSs.
gram according to a given logging specification. Furthermore, we detail and establish pertinent properties, notably including the correctness of the instrumentation algorithm.
duces a class of logging specifications adept at specifying temporal relations among computational events in hybrid-dynamic systems. Following this, Section 3.3 outlines the syntax and semantics of hybrid programs enriched with audit logging capabilities. Finally, in Section 3.4, we delve into the instrumentation algorithm and elucidate the properties it adheres.
O4 (, , O6 (, ,
= 1, 2 1 ∪ 2) ⟶ ( + 1, , ) 3.1. Source HP Model
↦ ] ⊨ . format. For example, i) ⊨ We consider HPs as our source language model, refered by . Syntax and semantics of HPs [12] are defined in the following, which are grounded in real arithmetic polynomial terms and FOL of real arithmetic.
We define polynomial terms with rational coeficients over a countably infinite set of variables . A polynomial term takes the form ∶∶= | | . | + , where ∈ and ∈ ℚ (a rational number). A state, , is a mapping from variables to real numbers, i.e., ∶ → ℝ . We let ∈ ℝ to range over real numbers throughout the paper. The semantics of a polynomial term is determined by a state, J K, given in the standard form. For example, J K = ( ), and J. ′K = J K. J ′K. ∶∶= = | ≥ | ¬ | ∧ | ∃ .
Additional syntactic structures, such as disjunction, implication, universal quantification, etc., can be defined using this minimal syntax. A state models a predicate , denoted by ⊨ in the standard = ′ if J K = J K ′ , and ii) ⊨ ∃ if there exists ∈ ℝ such that
The statement ∶= updates to the value of .
∶∶= ∶= | ∶=∗ updates
to a nondeterministic value. ( ̄ ) ∶=∗ | ( ̄ ) | ? | ′ = & | ∪ | ; | ∗. refers to invoking function with inputs ̄ . A codebase maps function names to their definitions: ( ̄ ) = . The statement ? is a boolean test. ′ = & is a continuous program with an ordinary diferential equation ′ = and an evolution domain , where ′ denotes the time derivative of .
such equations to specify a continuous evolution. We use ∪ for nondeterministic choice, ; for sequencing, and ∗ for iterating nondeterministic number of times. We show empty sequence of
where is the evaluation context and is defined as
and 2 structurally congruent, 1 ≡ 2 according to the following rules: i) Structural congruence is an equivalence relation. ii) ; ≡ . iii) ∗ ≡ 0 ∪ 1 ∪ ⋯ = ∪ ∈ℕ , where is the iteration for times, defined as 0 =?⊤ and +1 = ; . iv) 1 ≡ 2 implies [ 1] ≡ [ 2], ∶∶= [ ] | ; | ; .
p along with the codebase of all defined functions, i.e., p = ⟨ p, ⟩. We assume that p simply invokes the specific function ()
) where ∈ ℝ≥0 is a timestamp. Accordingly, we define the timestamped operational semantics of HPs in Figure 1. According to rule O1, ∶= updates the state by mapping to the value of in . In rule O2, is updated with being mapped to a nondeterministic real value. ? is defined only for states that model , without altering the state, according to rule O3. In rule O4, invoking with inputs ̄ runs the body of the function in a new state, where fresh parameter names are rule O8 states that reduction follows structural congruence. ing system, etc.) defined as is the computational component and ℎ mapped to their corresponding polynomial term values. According to rule O5, ′ = & is executable if there exists a solution for the equation ′ = in the domain . In this case, is updated according to ′ = within some nondeterministic continuous time span [0, ], where every state update must is the physical component of the AV (the engine, braksatisfy the domain condition . Rule O6 describes how 1 ∪ 2 1 and 2 to run. Rule O7 specifies reduction of sequences of HPs using an evaluation context, and nondeterministically chooses between Example 3.1. Having introduced HPs as the source language model, let’s revisit the AV example described in Section 1. We can describe the AV system as the HP ( ; ℎ ) ∗, where mental sensors to detect obstacles. Predicate 1 returns true if an obstacle is detected. Function analyzes the data to determine the threat level and appropriate response, e.g., braking level or maneuver. () = (); (), respectively. Function
() retrieves data from speed sensors and environ= ( (); (? 1; (); (? 2; ()) ∪ ?¬ 2) ∪ ?¬ 1)∗ and Predicate 2 returns true if the threat level is high enough for hard breaking. Function the hard braking command. In our language model, the command can be described by simply setting () executes () delineates the temporal progression of the AV’s position through the application of diferential the acceleration parameter to a proper negative value. Function physical evolution, e.g., time and acceleration (efectively coming from () assigns certain initial values for ()). Finally, the function equations. This function is formally expressed as ′ = 1, ′ = , ′ = & ≤ , where , , , and represent the time, position, velocity, and acceleration of the AV, respectively. Here, is a continuously increasing time variable. The evolution of the AV’s position, velocity, and timer is confined within its evoafter which control is transferred back to the lution domain, which imposes an upper limit on the driving duration—denoted by ≤ . This constraint ensures that the AV does not operate continuously beyond a pre-set limit of time units for safety reasons,
consider the following predicates to logically specify a trace: DAssign/3, NDAssign/2, Test/2, Call/3,
(⋅)
We have the following cases: i) If ≡
[ ∶= ] then we define the instantiation of the configura( ), which returns the logical specification of . Let = (, , ( ) = {DAssign(, , ), Context(, ), State(, )}. ii) If ≡ [ ∶=∗] then ℎ ration is defined as specification of configurations, using ification is defined as string literals to conform with the syntax of predicate logic.
We define the logical specification of traces for both finite and infinite cases based on the logical ( ) is injective and monotonically increasing can be done straightforwardly.
( ) ( ). Let
= 0 1 ⋯ for some , then its logical spec. Otherwise, for infinite trace = 0 1 ⋯, we have
( ′) = ⋃ =0 ( ), for ′ = 0 1 ⋯ . Showing {NDAssign(, ), Context(, ), State(, )}. iii) If ≡ [? ] then the instantiation of the configu( ) = {Test(, ), Context(, ), State(, )}. iv) If ≡ [ ( ̄ )] then we ( ) = {Call(, , ̄ ), Context(, ), State(, )}, v) If ≡ [ ′ = & ] then we define ( ) = {Continuum(, ′ = , ), Context(, ), State(, )}. vi) Finally, if ≡ [ 1 ∪ 2] then ( ) = {Choice(, 1, 2), Context(, ), State(, )}. In essence,
( ) specifies the evalua tion context and the redex within
. Note that HP constructs, evaluation contexts, and states appear as predicate arguments in this presentation to enhance readability. Their syntax can be expressed as in which for all ∈ {0, ⋯ , }
i) is a function name with a definition in , ii) ̄ is a placeholder for a sequence of parameters passed to , and iii) Call( , , ̄ ) specifies the event of invoking at time
triggers and logging events as follows: ( ) = { 1, ⋯ , } and
( ) = 0. The logging preconditions are predicates Call( , , ̄ ) for all ∈ {1, ⋯ , }. Example 3.2. We can define the guideline of the logging specification for the example in Section 1 and Example 3.1 as follows: where Γ is a set of Horn clauses referred to as guidelines, including clauses of the form 3.2. Instantiation of Logging Specifications cations in HPs. Formally, The class of logging specifications
is defined to specify temporal relations among function invois the set of all logging specifications given by (Γ , {LoggedCall}), 3.3. Target HP Model program in
log. they have fixed arities. is defined as 0 = (0, 0, ,
∅, ∅). ∀ 0, ⋯ , 3, ̄ 0, ⋯ , ̄ 3.
Call( 0, , ̄ 0) ∧ Call( 1, , ̄ 2) ∧ 1 < 0 ∧ Call( 2, , ̄ 2)∧ 2 < 0 ∧ Call( 3, , ̄ 3) ∧ 3 < 0 ∧ 3 < 2 ∧ 2 < 1 ⟹
LoggedCall(, are called in order before The guidelines ensures logging the invocations of () if the functions (). In this specification, we are skipping to list a detailed collection of diferent environmental variables, e.g., the location, speed, and acceleration. inputs for each function for the sake of brevity. As mentioned in Section 1, for instance, ̄ 0 could include
and semantics. The task of the instrumentation algorithm is to map a program specified in to a log, with the following syntax
log
with two additional components, as well. A configuration . These preconditions are supposed to be gathered, in order to decide whether to log an event. ∶∶= (, , ,
Σ, Λ), where Σ is a set of predicates of the form Call(, , ̄ ), where ∈ Λ is the audit log, i.e., the set of predicates of the form LoggedCall( , ̄ ). The initial configuration is The reduction semantics of
log is given below. Note that and Γ are part of runtime structure, but for the sake of breveity we avoid annotating each step of reduction with these static structures. ̄ 0). (), and (1) ()
NO_LOG
Σ ∪ Γ ⊬ LoggedCall( , J̄K) (, , emit ( , ̄); , Σ, Λ) ⟶ (, , , Σ, Λ) CONTEXT
(, , , Σ, Λ) ⟶ ( ′, ′, ′, Σ′, Λ′) (, , [ ], Σ, Λ) ⟶ ( ′, ′, [ ′], Σ′, Λ′) log inherits the operational semantics of via rule HP. Rule CALL_EV handles reduction with the callEvent( , ̄ ) statement, adding Call(, , J ̄ K) to Σ. For the emit ( , ̄ ) statement, rule LOG checks if the predicate LoggedCall( , ̄ ) is derivable from Σ and Γ . If so, it adds it to the audit log Λ; otherwise, there is no change to the log, as specified by rule NO_LOG.
The residual log of a configuration is given by ( ) = = Λ, where = (_, _, _, _, Λ). This instantiation defines ⇝ for log. Since consists of logical literals, ( ) = adequately specifies ⌊ ⌋. 3.4. Instrumentation of HPs In this section, we discuss the instrumentation algorithm tailored for audit logging in HPs. Next, we review how the semantic preservation can be defined for this algorithm. Lastly, we specify the main results.
Instrumentation algorithm Instrumentation algorithm takes an program p = ⟨, ⟩ and a logging specification ∈ , and produces a program p′ = ⟨ p, ′⟩ in log. The details of how modifies the codebase is given in the following. Let ( ) = [ ( ̄ ) = ]. We have three cases: i) If ∈ ( ) then ′( ) = [ ( ̄ ) = callEvent( , ̄ ); ]. ii) If ∈ ( ) then ′( ) = [ ( ̄ ) = callEvent( , ̄ ); emit ( , ̄ ); ]. iii) If ∉ ( ) ∪ ( ) then ′( ) = ( ). Intuitively, with the invocation of a function , i) If the invocation of serves as a trigger, its execution must be preceded by a callEvent statement. Consequently, the invocation of is recorded in the set of logging preconditions Σ, as outlined by the rule CALL_EV. ii) If the invocation of constitutes a logging event, its execution must also be preceded by a callEvent statement, similar to the previous scenario. Subsequently, the system evaluates whether this invocation should be logged, which is determined by the presence of an emit statement (covered by rules LOG and NO_LOG). Following this evaluation, proceeds with its execution as usual. If the invocation of does not serve as a trigger nor a logging event, then the function executes without any alteration in behavior. Example 3.3. For the logging specification in Example 3.2, injects statements callEvent(, ̄ ), callEvent( , ̄ ) and callEvent( , ̄ ) to the beginning of functions (), () and (), respectively, as these functions are triggers to log. Since () is the logging event, modifies the body of the function to be callEvent(, ̄ ); emit (, ̄ ); ( ′ = 1, ′ = , ′ = & ≤ ). Instantiation of trace correspondence relation ∶≈ We instantiate the abstraction of the correspondence relation ∶≈ between source and target traces for . We establish the source and target trace correspondence relation as follows: 1 1 ∶≈ 2 2 if 1 = (, , 1), 2 = (, , 2, Σ, Λ), and ( 2) = 1. The function essentially eliminates any callEvent and emit statements that may introduce to an HP. ii) ( 1 ∪ 2) = v) Otherwise,
can be defined as follows: i) ( 2). iii) ( 1; 2) =
(callEvent( , ̄ )) = ( 1); ( 2). iv)
(emit ( , ̄ )) = . ( ∗) = ( ( ))∗.
Main Results Main properties include two results. The instrumentation algorithm is semantics preserving, and is correct. Proofs of the theorems are given in the accompanying technical report [13].
Hybrid-dynamic models may use programming languages techniques to specify CPSs, particularly through HPs, as we have employed in this paper. Along with HPs, there are two other major approaches to formally model CPSs: Hybrid automata, which describe a hybrid system through a finite state transition system that captures both discrete and continuous variables in each state [14, 15], and hybrid process calculi [16, 17, 18, 19], which model CPSs in terms of agents representing physical plants and cyber components. These agents communicate through named channels, and in systems like CCPS [18], a labeled transition system demonstrates how such agents execute using shared channels.
cybersecurity assurance in this domain [20]. More recent examples include developing an accountability system for autonomous robots [21], a microservices-based architecture for industrial Internet of Things and CPSs [22], and enhancing realtime CPSs with audit logging capabilities [6, 23]. These proposals have architectural approaches to audit logging, whereas we study audit logging from a programming point of view and establish formal guarantees about the quality of the generated logs in
correct audit logging in diferent realms of computation, initially in linear functional settings [8].
This paper introduces an algorithm designed to implement precise audit logging in CPSs by instrumenting hybrid programs according to formal audit logging requirements specified using Horn clause logic. Our approach maintains the original program’s semantics, altering only audit-related operations. We prove that our algorithm consistently produces accurate audit logs, efectively avoiding unnecessary or missing logging events.
[2] M. Lehto, Cyber-attacks against critical infrastructure, in: Cyber security: Critical infrastructure protection, Springer, 2022, pp. 3–42. [3] T. Alladi, V. Chamola, S. Zeadally, Industrial control systems: Cyberattack trends and countermeasures, Computer Communications 155 (2020) 1–8. [4] K. Kim, J. S. Kim, S. Jeong, J.-H. Park, H. K. Kim, Cybersecurity for autonomous vehicles: Review of attacks and defense, Computers & security 103 (2021) 102150. [5] P. Kumar, Y. Lin, G. Bai, A. Paverd, J. S. Dong, A. Martin, Smart grid metering networks: A survey on security, privacy and open research issues, IEEE Communications Surveys & Tutorials 21 (2019) 2886–2927. [6] A. Bansal, A. Kandikuppa, C.-Y. Chen, M. Hasan, A. Bates, S. Mohan, Towards eficient auditing for real-time systems, in: ESORICS, Springer, 2022, pp. 614–634. [7] J. Kohlas, J. Schmid, An algebraic theory of information: An introduction and survey, Information 5 (2014) 219–254. [8] S. Amir-Mohammadian, S. Chong, C. Skalka, Correct audit logging: Theory and practice, in:
Principals of Security and Trust, 2016, pp. 139–162. [9] S. Amir-Mohammadian, C. Kari, Correct audit logging in concurrent systems, Electronic Notes in Theoretical Computer Science 351 (2020) 115–141. [10] A. Platzer, Diferential dynamic logic for hybrid systems, Journal of Automated Reasoning 41 (2008) 143–189. [11] A. Platzer, The complete proof theory of hybrid systems, in: 2012 27th Annual IEEE Symposium on Logic in Computer Science, IEEE, 2012, pp. 541–550. [12] A. Platzer, Logical foundations of cyber-physical systems, volume 662, Springer, 2018. [13] S. Amir-Mohammadiah, Technical Report: Correct Audit Logging in Hybrid-Dynamic Systems,
[14] R. Alur, C. Courcoubetis, T. A. Henzinger, P.-H. Ho, Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems, in: Hybrid systems, Springer, 1992, pp. 209–229. [15] T. A. Henzinger, The theory of hybrid automata, in: Verification of digital and hybrid systems,
Springer, 2000, pp. 265–292. [16] V. Galpin, L. Bortolussi, J. Hillston, Hype: Hybrid modelling by composition of flows, Formal
Aspects of Computing 25 (2013) 503–541. [17] I. Lanese, L. Bedogni, M. Di Felice, Internet of things: a process calculus approach, in: SAC, 2013, pp. 1339–1346. [18] R. Lanotte, M. Merro, A calculus of cyber-physical systems, in: ICALP, Springer, 2017, pp.
115–127. [19] R. Lanotte, M. Merro, A semantic theory of the internet of things, Information and Computation 259 (2018) 72–101. [20] R. Mitchell, I.-R. Chen, A survey of intrusion detection techniques for cyber-physical systems,
ACM Computing Surveys (CSUR) 46 (2014) 1–29. [21] L. Fernández-Becerra, Á. Manuel Guerrero-Higueras, F. J. Rodríguez-Lera, V. Matellán, Accountability as a service for robotics: Performance assessment of diferent accountability strategies for autonomous robots, Logic Journal of the IGPL 32 (2024) 243–262. [22] J. Dobaj, J. Iber, M. Krisper, C. Kreiner, A microservice architecture for the industrial internetof-things, in: EuroPLoP), 2018, pp. 1–15. [23] A. Bansal, A. Kandikuppa, M. Hasan, C.-Y. Chen, A. Bates, S. Mohan, System auditing for realtime systems, TOPS 26 (2023) 1–37. [24] S. Amir-Mohammadian, C. Skalka, In-depth enforcement of dynamic integrity taint analysis, in:
2016, pp. 43–56. [25] C. Skalka, S. Amir-Mohammadian, S. Clark, Maybe tainted data: Theory and a case study, Journal of Computer Security 28 (2020) 295–335. [26] S. Amir-Mohammadian, A. Y. Zowj, Towards concurrent audit logging in microservices, in:
STPSA 2021, 2021, pp. 1357–1362. [27] N. D. Ahn, S. Amir-Mohammadian, Instrumenting microservices for concurrent audit logging: Beyond Horn clauses, in: STPSA 2022, 2022, pp. 1762–1767.