An Approach for Network Information Flow Analysis for Systems of Embedded Components

  • Andrey Chechulin
  • Igor Kotenko
  • Vasily Desnitsky
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7531)


Systems (devices) with embedded components operate in a potentially hostile environment and have strong recourse limitations. The development of security-enhanced embedded components is a complicated task owning to different types of threats and attacks that may affect the device, and because the security in embedded devices is commonly provided as an additional feature at the final stages of the development process, or even neglected. In the paper we consider an approach to analysis of network information flows in systems containing embedded components. This approach helps to the system engineer to evaluate the embedded system from security point of view and to correct the architecture of future system on early stages of the development.


information flows embedded devices model checking topology analysis 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Desnitsky, V., Kotenko, I., Chechulin, A.: An Abstract Model for Embedded Systems and Intruders. In: Proceedings of the Work in Progress Session Held in Connection with the 19th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (PDP 2011), pp. 25–26. SEA-Publications, SEA-SR-29 (2011)Google Scholar
  2. 2.
    Desnitsky, V., Chechulin, A.: Model of the Process for Secure Embedded Systems Development. High Availability Systems (2), 97–101 (2011) (in Russian) Google Scholar
  3. 3.
    Kotenko, I., Desnitsky, V., Chechulin, A.: Investigation of Technologies for Secure Embedded Systems Design in European Union Project SecFutur. Information Security Inside (3), 68–75 (2011) (in Russian) Google Scholar
  4. 4.
    Desnitsky, V., Kotenko, I., Chechulin, A.: Constructing and Testing Secure Embedded Systems. In: Selected Proceedings of XII Saint-Petersburg International Conference “Regional informatics-2010” (“RI-2010”), pp. 115–121. St. Petersburg (2011) (in Russian)Google Scholar
  5. 5.
    Rushby, J.: Noninterference, Transitivity, and Channel-control Security Policies, SRI International. Tech. Rep. CSL-92-02 (1992)Google Scholar
  6. 6.
    von Oheimb, D.: Information Flow Control Revisited: Noninfluence = Noninterference + Nonleakage. In: Samarati, P., Ryan, P.Y.A., Gollmann, D., Molva, R. (eds.) ESORICS 2004. LNCS, vol. 3193, pp. 225–243. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  7. 7.
    Lampson, B.: A note on the confinement problem. Communications of ACM 16(10), 613–615 (1973)CrossRefGoogle Scholar
  8. 8.
    Pistoia, M., Chandra, S., Fink, S., Yahav, E.: A Survey of Static Analysis Methods For Identifying Security Vulnerabilities in Software Systems. IBM Systems Journal 46(2), 265–288 (2007)CrossRefGoogle Scholar
  9. 9.
    Hedin, D., Sabelfeld, A.: A Perspective on Information-Flow. Summer school Control Tools for Analysis and Verification of Software Safety and Security, Marktoberdorf, Germany (2011)Google Scholar
  10. 10.
    Sabelfeld, A., Myers, A.C.: Language-based Information-flow Security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)CrossRefGoogle Scholar
  11. 11.
    SecFutur project website,
  12. 12.
    Ahlswede, R., Cai, N., Li, S.-Y.R., Yeung, R.W.: Network Information Flow. IEEE Transactions on Information Theory IT-46(4), 1204–1216 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  13. 13.
    Sprintson, A., El Rouayheb, S., Georghiades, C.: A New Construction Method for Networks from Matroids. In: Proceedings of the 2009 IEEE International Conference on Symposium on Information Theory (ISIT 2009), Seoul (2009)Google Scholar
  14. 14.
    Agaskar, A., He, T., Tong, L.: Distributed Detection of Multi-hop Information Flows with Fusion Capacity Constraints. IEEE Transactions on Signal Processing 58(6), 3373–3383 (2010)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Rae, A., Fidge, C.: Information Flow Analysis for Fail-Secure Devices. The Computer Journal 48(1), 17–26 (2005)CrossRefGoogle Scholar
  16. 16.
    Cabuk, S., Brodley, C.E., Shields, C.: IP Covert Channel Detection. ACM Transactions on Information and System Security (2008)Google Scholar
  17. 17.
    Berk, V., Giani, A., Cybenko, G.: Detection of Covert Channel Encoding in Network Packet Delays. Technical Report TR536 (2005)Google Scholar
  18. 18.
    Shnayder, V.: Opportunities for Language Based Information Flow Security in Sensor Networks (2004)Google Scholar
  19. 19.
    Gruska, D.P.: Network Information Flow. Fundamentae Informaticae 72(1-3), 167–180 (2006)MathSciNetzbMATHGoogle Scholar
  20. 20.
    Gruska, D.P., Maggiolo-Schettini, A.: Process Algebra for Network Communication. Fundamenta Informaticae 45(4), 359–378 (2001)MathSciNetzbMATHGoogle Scholar
  21. 21.
    Al-Shaer, E., Hamed, H., Boutaba, R., Hasan, M.: Conflict Classification and Analysis of Distributed Firewall Policies. IEEE Journal on Selected Areas in Communications (JSAC) 23(10) (2005)Google Scholar
  22. 22.
    Al-Shaer, E., El-Atawy, A., Samak, T.: Automated Pseudo-live Testing of Firewall Configuration Enforcement. IEEE Journal on Selected Areas in Communications 27(3), 302–314 (2009)CrossRefGoogle Scholar
  23. 23.
    Feamster, N., Balakrishnan, H.: Detecting BGP Configuration Faults with Static Analysis. NSDI (2005)Google Scholar
  24. 24.
    Bush, R., Griffin, T.: Integrity for virtual private routed networks. IEEE INFOCOM 2003 2, 1467–1476 (2003)Google Scholar
  25. 25.
    Al-Shaer, E., Marrero, W., El-Atawy, A., El-Badawi, K.: Network Configuration in A Box: Towards End-to-End Verification of Network Reachability and Security. In: 17th IEEE International Conference on Network Protocols (ICNP 2009), pp. 123–132 (2009)Google Scholar
  26. 26.
    Emerson, E.A.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, ch. 16, vol. B, pp. 995–1072. MIT Press (1990)Google Scholar
  27. 27.
    Bryant, R.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)Google Scholar
  28. 28.
  29. 29.
    McComb, T., Wildman, L.: User guide for SIFA v.1.0. Technical report (2006)Google Scholar
  30. 30.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press (2008)Google Scholar
  31. 31.
    Kotenko, I., Polubelova, O.: Verification of Security Policy Filtering Rules by Model Checking. In: Proceedings of IEEE Fourth International Workshop on Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications (IDAACS 2011), pp. 706–710 (2011)Google Scholar
  32. 32.
    Holzmann, G.: The Spin Model Checker Primer and Reference Manual. Addison-Wesley (2003)Google Scholar
  33. 33.
    McMillan, K.: The SMV System,
  34. 34.
    Alur, R., Anand, H., Grosu, R., Ivancic, F., et al.: Mocha User Manual. Jmocha Version 2.0,

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Andrey Chechulin
    • 1
  • Igor Kotenko
    • 1
  • Vasily Desnitsky
    • 1
  1. 1.St. Petersburg Institute for Informatics and Automation (SPIIRAS)St. PetersburgRussia

Personalised recommendations