[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Symbolic Execution for Precise Information Flow Analysis of Timed Concurrent Systems

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 15280))

Included in the following conference series:

  • 91 Accesses

Abstract

Information flow analysis (IFA) is a powerful technique for verifying confidentiality and integrity. This is highly desirable for embedded systems, where security violations can lead to significant economic damages or even loss of human life. Unfortunately, if shared bus architectures are used, classical IFA that do not consider timing behavior will always classify the whole system as insecure. In this paper, we present an approach to regain precision in IFA for timed systems that concurrently execute processes using a cooperative scheduler. Our key idea is to extend a classical IFA approach based on program dependence graphs with a symbolic execution together with abstract interpretation to precisely yet abstractly capture data, control, timing, and event dependencies between processes. While this increases the cost of the analysis, the gain in precision leverages IFA even for concurrent systems with time-shared bus architectures as they are widely used, for example, in the automotive industry. We have implemented our approach for the system level description language SystemC, and demonstrate its applicability with a case study that uses a general-purpose input/ouput (GPIO).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 49.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 59.99
Price includes VAT (United Kingdom)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    SystemC allows for more complex process states, e.g. waiting for one or all of several events or combining waiting for events with a timeout. We omit this in the definition, but our prototypical implementation can handle such complex process states.

  2. 2.

    A reproduction package including the implementation and all examples discussed in this paper can be found at https://doi.org/10.5281/zenodo.12584236.

  3. 3.

    Executed with Java 21 on an AMD Ryzen 9 5900X with 6.5 GB of RAM available to the JVM and without use of parallelization in the analysis.

References

  1. Chattopadhyay, S., Beck, M., Rezine, A., Zeller, A.: Quantifying the information leakage in cache attacks via symbolic execution. ACM Trans. Embed. Comput. Syst. 18(1), 7:1–7:27 (2019)

    Google Scholar 

  2. Cimatti, A., Narasamdya, I., Roveri, M.: Software model checking SystemC. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 32(5), 774–787 (2013)

    Google Scholar 

  3. Coughlin, N., Smith, G.: Rely/guarantee reasoning for noninterference in non-blocking algorithms. In: IEEE Computer Security Foundations Symposium, CSF, pp. 380–394 (2020)

    Google Scholar 

  4. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM Symposium on Principles of Programming Languages, pp. 238–252 (1977)

    Google Scholar 

  5. Davidson, D., Moench, B., Ristenpart, T., Jha, S.: FIE on firmware: finding vulnerabilities in embedded systems using symbolic execution. In: USENIX Security Symposium, pp. 463–478 (2013)

    Google Scholar 

  6. Eilers, M., Dardinier, T., Müller, P.: CommCSL: proving information flow security for concurrent programs using abstract commutativity. Proc. ACM Program. Lang. 7(PLDI), 1682–1707 (2023)

    Google Scholar 

  7. Ernst, G., Murray, T.: SecCSL: security concurrent separation logic. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 208–230. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25543-5_13

    Chapter  Google Scholar 

  8. Focardi, R., Gorrieri, R., Martinelli, F.: Real-time information flow analysis. IEEE J. Sel. Areas Commun. 21(1), 20–35 (2003)

    Article  Google Scholar 

  9. Fowze, F., Choudhury, M., Forte, D.: Eisec: exhaustive information flow security of hardware intellectual property utilizing symbolic execution. In: Asian Hardware Oriented Security and Trust Symposium, AsianHOST, pp. 1–6 (2022)

    Google Scholar 

  10. Gerking, C., Schubert, D., Bodden, E.: Model checking the information flow security of real-time systems. In: Engineering Secure Software and Systems - International Symposium, ESSoS. vol. 10953, pp. 27–43 (2018)

    Google Scholar 

  11. Giffhorn, D., Snelting, G.: A new algorithm for low-deterministic security. Int. J. Inf. Sec. 14(3), 263–287 (2015)

    Article  Google Scholar 

  12. Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, pp. 11–20 (1982)

    Google Scholar 

  13. Habibi, A., Moinudeen, H., Tahar, S.: Generating finite state machines from SystemC. In: Design, Automation and Test in Europe (DATE), pp. 76–81 (2006)

    Google Scholar 

  14. Hammer, C., Snelting, G.: An improved slicer for java. In: ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE, pp. 17–22 (2004)

    Google Scholar 

  15. Hecker, M., Bischof, S., Snelting, G.: On time-sensitive control dependencies. ACM Trans. Program. Lang. Syst. 44(1), 2:1–2:37 (2022)

    Google Scholar 

  16. Herber, P., Hünnemeyer, B.: Formal verification of SystemC designs using the BLAST software model checker. In: ACESMB@ MoDELS, pp. 44–53 (2014)

    Google Scholar 

  17. Herber, P., Pockrandt, M., Glesner, S.: STATE – a SystemC to timed automata transformation engine. In: ICESS (2015)

    Google Scholar 

  18. Herdt, V., Le, H.M., Große, D., Drechsler, R.: Verifying SystemC using intermediate verification language and stateful symbolic simulation. IEEE Trans. Comput-Aided Des. Integr. Circuits Syst. 38(7), 1359–1372 (2018)

    Google Scholar 

  19. Horwitz, S., Reps, T.W., Binkley, D.W.: Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst. 12(1), 26–60 (1990)

    Article  Google Scholar 

  20. Hsieh, C.S., Unger, E.A., Mata-Toledo, R.A.: Using program dependence graphs for information flow control. J. Syst. Softw. 17(3), 227–232 (1992)

    Article  Google Scholar 

  21. IEEE Standards Association: IEEE Std. 1666–2011, Open SystemC Language Reference Manual. IEEE Press (2011)

    Google Scholar 

  22. Jaß, L., Herber, P.: Bit-precise formal verification for SystemC using satisfiability modulo theories solving. In: International Embedded Systems Symposium (IESS) (2015)

    Google Scholar 

  23. Karbyshev, A., Svendsen, K., Askarov, A., Birkedal, L.: Compositional non-interference for concurrent programs via separation and framing. In: Principles of Security and Trust - International Conference, POST, vol. 10804, pp. 53–78 (2018)

    Google Scholar 

  24. Karlsson, D., Eles, P., Peng, Z.: Formal verification of SystemC designs using a petri-net based representation. In: Design, Automation and Test in Europe (DATE), pp. 1228–1233 (2006)

    Google Scholar 

  25. King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)

    Article  MathSciNet  Google Scholar 

  26. Krinke, J.: Context-sensitive slicing of concurrent programs. In: ACM SIGSOFT Symposium on Foundations of Software Engineering, FSE, pp. 178–187 (2003)

    Google Scholar 

  27. Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Time and probability-based information flow analysis. IEEE Trans. Softw. Eng. 36(5), 719–734 (2010)

    Article  Google Scholar 

  28. Man, K.L., Fedeli, A., Mercaldi, M., Boubekeur, M., Schellekens, M.P.: SC2SCFL: automated SystemC to SystemCFL translation. In: Embedded Computing Systems: Architectures, Modeling, and Simulation, pp. 34–45 (2007)

    Google Scholar 

  29. Mantel, H., Sabelfeld, A.: A generic approach to the security of multi-threaded programs. In: IEEE Computer Security Foundations Workshop (CSFW), pp. 126–142. IEEE Computer Society (2001)

    Google Scholar 

  30. Mantel, H., Sands, D., Sudbrock, H.: Assumptions and guarantees for compositional noninterference. In: IEEE Computer Security Foundations Symposium, CSF, pp. 218–232 (2011)

    Google Scholar 

  31. Mantel, H., Sudbrock, H.: Types vs. PDGs in information flow analysis. In: Logic-Based Program Synthesis and Transformation: International Symposium, LOPSTR, pp. 106–121 (2013)

    Google Scholar 

  32. Murray, T.C., Sison, R., Engelhardt, K.: COVERN: a logic for compositional verification of information flow control. In: IEEE European Symposium on Security and Privacy, EuroS &P, pp. 16–30 (2018)

    Google Scholar 

  33. Nanda, M.G., Ramesh, S.: Interprocedural slicing of multithreaded programs with applications to Java. ACM Trans. Program. Lang. Syst. 28(6), 1088–1144 (2006)

    Article  Google Scholar 

  34. Nielson, F., Nielson, H.R., Vasilikos, P.: Information flow for timed automata. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 3–21. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63121-9_1

    Chapter  Google Scholar 

  35. Phan, Q., Malacaria, P., Tkachuk, O., Pasareanu, C.S.: Symbolic quantitative information flow. ACM SIGSOFT Softw. Eng. Notes 37(6), 1–5 (2012)

    Article  Google Scholar 

  36. Ryan, K., Gregoire, M., Sturton, C.: SEIF: augmented symbolic execution for information flow in hardware designs. In: International Workshop on Hardware and Architectural Support for Security and Privacy, HASP, pp. 1–9 (2023)

    Google Scholar 

  37. Schoepe, D., Murray, T., Sabelfeld, A.: VERONICA: expressive and precise concurrent information flow security. In: IEEE Computer Security Foundations Symposium, CSF, pp. 79–94 (2020)

    Google Scholar 

  38. Schwan, S., Herber, P.: Optimized hardware/software co-verification using the UCLID satisfiability modulo theory solver. In: International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE, pp. 225–230 (2020)

    Google Scholar 

  39. Snelting, G.: Combining slicing and constraint solving for validation of measurement software. In: Static Analysis, International Symposium, SAS, vol. 1145, pp. 332–348 (1996)

    Google Scholar 

  40. Subramanyan, P., Malik, S., Khattri, H., Maiti, A., Fung, J.M.: Verifying information flow properties of firmware using symbolic execution. In: Design, Automation and Test in Europe Conference and Exhibition, DATE, pp. 337–342 (2016)

    Google Scholar 

  41. Tasche, P., Monti, R.E., Drerup, S.E., Blohm, P., Herber, P., Huisman, M.: Deductive verification of parameterized embedded systems modeled in SystemC. In: Verification, Model Checking, and Abstract Interpretation, pp. 187–209 (2024)

    Google Scholar 

  42. Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2–3), 167–187 (1996)

    Article  Google Scholar 

  43. Weiser, M.D.: Program slicing. IEEE Trans. Softw. Eng. 10(4), 352–357 (1984)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, University of Münster, Münster, Germany

    Jonas Becker-Kupczok & Paula Herber

Authors
  1. Jonas Becker-Kupczok
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paula Herber
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jonas Becker-Kupczok .

Editor information

Editors and Affiliations

  1. Campus Gualtar, University of Aveiro, Aveiro, Portugal

    Alexandre Madeira

  2. University of Augsburg, Augsburg, Germany

    Alexander Knapp

Rights and permissions

Reprints and permissions

Copyright information

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Becker-Kupczok, J., Herber, P. (2025). Symbolic Execution for Precise Information Flow Analysis of Timed Concurrent Systems. In: Madeira, A., Knapp, A. (eds) Software Engineering and Formal Methods. SEFM 2024. Lecture Notes in Computer Science, vol 15280. Springer, Cham. https://doi.org/10.1007/978-3-031-77382-2_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-77382-2_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-77381-5

  • Online ISBN: 978-3-031-77382-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation