Main Objectives

One of the primary objectives of the SINCRET project is to investigate and formulate the theory (and the corresponding monitor synthesis tools) related to incremental/compositionality of enforcers in the timed context. We will initially consider the enforcement monitor synthesis framework suitable for reactive CPS proposed in [PRSTH17] for discrete timed properties. We will study/explore various schemes for incrementally adding/composing enforcers in such frameworks. We will consider various schemes for composing enforcers such as serial and parallel composition schemes, and find out which sub-class of properties are enforceable incrementally using these different schemes. In addition to theory and the monitor synthesis tools, we will also explore pros/cons of these schemes using application scenarios related to security of CPSs.

Objective 1: Incremental/compositional RE-reactive/synchronous framework for safety (timed) properties.

We will consider enforcement of policies expressed as discrete timed automata. Under objective 1, we will focus on the safety subclass of properties, and study the incremental schemes for the safety subclass. For incremental/scalable enforcement, we will consider multiple schemes for composing enforcers. Under milestone 1, we will focus on the serial approach for composing enforcers. Our milestone 2 under this objective is to explore the parallel scheme for composing enforcers. The planned deliverables are (1) Theory of composition of enforcers (reactive/synchronous setting) in series and parallel for safety timed properties- constraints, definitions, algorithms; (2) Implementation of a prototype framework (3) Comparison of both serial and parallel schemes, evaluation using example scenarios;

Objective 2: Incremental/compositional RE-reactive/synchronous framework for all regular (timed) properties

We will focus on extending the study and results to all regular timed properties. Under milestone 1, we will look into the serial scheme for all regular timed properties, and under milestone 2 we will focus on the parallel scheme. The planned deliverables are (1) Theory of composition of enforcers (reactive/synchronous setting) in series and parallel for regular timed properties- constraints, definitions, algorithms; (2) enforceability conditions identifying which subclass of properties are enforceable using a particular incremental/compositional scheme; (2) Implementation of a prototype framework (3) Comparison of both serial and parallel schemes, evaluation using example scenarios;

Objective 3: Application of the proposed incremental enforcement frameworks in some specific application domains/scenarios; study distribution of enforcers;

We will also focus on illustration of the applicability and usefulness of the proposed incremental enforcement schemes in different application domains such as medical IoT, Autonomous vehicles, Drone swarms etc. We will specifically focus on illustrating how some of the security issues/concerns in these applications can be addressed using the proposed incremental monitoring schemes. In addition, we will also begin our study/exploration on other related problems such as distribution of enforcers (deploy enforcers in a distributed setting); and considering real-time properties. The planned deliverables are; (1) For two application domains, implementation of the required scenarios for assessments/evaluation/analysis; (2) Assessment using different sets of policies for enforcement; (3) Research report + Publication of these outcomes in suitable conferences/journals; (4) preliminary exploration of potential related problems such as approaches for distribution of enforcers will help us to clearly formulate/plan other problems that we can jointly work on in the future.

[Lee08] E. A. Lee, "Cyber Physical Systems: Design Challenges," 2008 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC), Orlando, FL, USA, 2008, pp. 363-369, doi: 10.1109/ISORC.2008.25.

[Lou15] G. Loukas, Cyber-Physical Attacks: A Growing Invisible Threat. London, U.K.: Butterworth, 2015.

[HLLL17] A. Humayed, J. Lin, F. Li, and B. Luo, ‘‘Cyber-physical systems security—A survey,’’ IEEE Internet Things J., vol. 4, no. 6, pp. 1802–1831, Dec. 2017

[Lan13] R. Langner, “To kill a centrifuge: A technical analysis of what stuxnets creators tried to achieve,” The Langner Group, 2013.

[LAC14] R. M. Lee, M. J. Assante, and T. Conway, “German steel mill cyber attack,” Industrial Control Systems, vol. 30, no. 62, pp. 1–15, 2014.

[CNN21] CNN, “Colonial pipeline ceo admits to authorizing 4.4 million ransomware payment,” 2021. [Online]. Available: https://edition.cnn.com/2021/05/19/politics/colonial-pipeline-ransom/index.html

[KKSV17] C. Kolias, G. Kambourakis, A. Stavrou, and J. Voas, “Ddos in the iot: Mirai and other botnets,” Computer, vol. 50, no. 7, pp. 80–84, 2017.

[BI17] E. Bertino and N. Islam, “Botnets and internet of things security,” Computer, vol. 50, no. 2, pp. 76–79, 2017.

[YNSC20] J.-P. Yaacoub, H. Noura, O. Salman, and A. Chehab, ‘‘Security analysis of drones systems: Attacks, limitations, and recommendations,’’ Internet Things, vol. 11, Sep. 2020, Art. no. 100218.

[PZ06] A. Pnueli and A. Zaks, “Psl model checking and run-time verification via testers,” in FM 2006: Formal Methods: 14th International Symposium on Formal Methods, Hamilton, Canada, August 21-27, 2006. Proceedings 14. Springer, 2006, pp. 573–586.

[BLS10] A. Bauer, M. Leucker, and C. Schallhart, “Comparing ltl semantics for runtime verification,” Journal of Logic and Computation, vol. 20, no. 3, pp. 651–674, 2010

[FFM09] Y. Falcone, J.-C. Fernandez, and L. Mounier, “Runtime verification of safety-progress properties,” in International Workshop on Runtime Verification. Springer, 2009, pp. 40–59.

[BLS11] Andreas Bauer, Martin Leucker, and Christian Schallhart. 2011. Runtime Verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20, 4, Article 14 (September 2011), 64 pages. https://doi.org/10.1145/2000799.2000800

[Sch00] F. B. Schneider, “Enforceable security policies,” ACM Trans. Inf. Syst. Secur., vol. 3, no. 1, pp. 30–50, 2000.

[LBW09] J. Ligatti, L. Bauer, and D. Walker, “Run-time enforcement of nonsafety policies,” ACM Trans. Inf. Syst. Secur., vol. 12, no. 3, pp. 19:1–19:41, Jan. 2009.

[YMFR11] Y. Falcone, L. Mounier, J.-C. Fernandez, and J.-L. Richier, “Runtime enforcement monitors: composition, synthesis, and enforcement abilities,” FMSD, vol. 38, no. 3, pp. 223–262, 2011

[PFJMRN14] S. Pinisetty, Y. Falcone, T. Jéron, H. Marchand, A. Rollet, and O. Nguena Timo, “Runtime enforcement of timed properties revisited,” FMSD, vol. 45, no. 3, pp. 381–422, 2014.

[NMMP15] M. Ngo, F. Massacci, D. Milushev, and F. Piessens, ‘‘Runtime enforcement of security policies on black box reactive programs,’’ in Proc. 42nd Annu. ACM SIGPLAN-SIGACT Symp. Princ. Program. Lang., Jan. 2015, pp. 43–54.

[PKRP19] H. Pearce, M. M. Y. Kuo, P. S. Roop, and S. Pinisetty, ‘‘Securing implantable medical devices with runtime enforcement hardware,’’ in Proc. 17th ACM-IEEE Int. Conf. Formal Methods Models Syst. Design, Oct. 2019, pp. 1–9.

[PT16] S. Pinisetty and S. Tripakis, ‘‘Compositional runtime enforcement,’’ in Proc. NASA Formal Methods Symp. (NFM). Minneapolis, MN, USA: Springer, 2016, pp. 82–99

[PPRT22] S. Pinisetty, A. Pradhan, P. Roop, and S. Tripakis, ‘‘Compositional runtime enforcement revisited,’’ Formal Methods Syst. Des., vol. 59, pp. 205–252, Oct. 2022

[PRSTH17] S. Pinisetty, P. S. Roop, S. Smyth, S. Tripakis, and R. V. Hanxleden, ‘‘Runtime enforcement of reactive systems using synchronous enforcers,’’ in Proc. 24th ACM SIGSOFT Int. SPIN Symp. Model Checking Softw., Santa Barbara, CA, USA, Jul. 2017, pp. 80–89.

[PRSATH17] S. Pinisetty, P. S. Roop, S. Smyth, N. Allen, S. Tripakis, and R. V. Hanxleden. Runtime enforcement of cyber-physical systems. ACM Trans. Embed. Comput. Syst., 16(5s):178:1–178:25, Sept. 2017.

[PBPR23] A. Panda, A. Baird, S. Pinisetty, and P. Roop, “Incremental security enforcement for cyber-physical systems,” IEEE Access, vol. 11, pp. 18 475–18 498, 2023.