Advertisement

X-by-C: Non-functional Security Challenges

  • Thomas Given-WilsonEmail author
  • Axel Legay
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11244)

Abstract

Correctness-by-Construction (C-by-C) approaches software development as formal engineering and builds correct code by iterating from a correct specification. However, C-by-C is focused on functional properties of the system. X-by-Construction (X-by-C) extends C-by-C to also consider non-function properties concerning aspects such as security, dependability, reliability or energy consumption. In this work we consider the challenges of applying X-by-C to non-functional security properties such as side-channel attacks. We demonstrate how such non-functional security can be captured and reasoned about in an X-by-C manner, yielding the benefit of C-by-C for non-functional properties and security challenges.

References

  1. 1.
    Amey, P.: Correctness by construction: better can also be cheaper. CrossTalk: J. Def. Softw. Eng. 2, 24–28 (2002)Google Scholar
  2. 2.
    Appel, A.W.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)CrossRefGoogle Scholar
  3. 3.
    Attie, P., Baranov, E., Bliudze, S., Jaber, M., Sifakis, J.: A general framework for architecture composability. Form. Asp. Comput. 28(2), 207–231 (2016)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Barnes, J.G.P.: High Integrity Ada: The SPARK Approach, vol. 189. Addison-Wesley, Reading (1997)Google Scholar
  5. 5.
    ter Beek, M., Carmona Vargas, J., Kleijn, J.: Communication and compatibility in systems of systems: correctness-by-construction. ERCIM News 2015(102), 21–22 (2015)Google Scholar
  6. 6.
    Bernstein, D.J.: Cache-timing attacks on AES (2005)Google Scholar
  7. 7.
    Bogdanov, A., et al.: PRESENT: an ultra-lightweight block cipher. In: Paillier, P., Verbauwhede, I. (eds.) CHES 2007. LNCS, vol. 4727, pp. 450–466. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-74735-2_31CrossRefGoogle Scholar
  8. 8.
    Bradley, M., Cassez, F., Fehnker, A., Given-Wilson, T., Huuck, R.: High performance static analysis for industry. Electron. Notes Theor. Comput. Sci. 289, 3–14 (2012)CrossRefGoogle Scholar
  9. 9.
    Brady, E., Hammond, K.: Correct-by-construction concurrency: using dependent types to verify implementations of effectful resource usage protocols. Fundam. Inform. 102(2), 145–176 (2010)zbMATHGoogle Scholar
  10. 10.
    Chapman, R.: Correctness by construction: a manifesto for high integrity software. In: Proceedings of the 10th Australian Workshop on Safety Critical Systems and Software, vol. 55, pp. 43–46. Australian Computer Society Inc. (2006)Google Scholar
  11. 11.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  12. 12.
    Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265–284. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54792-8_15CrossRefGoogle Scholar
  13. 13.
    Emerson, E.A.: The beginning of model checking: a personal perspective. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 27–45. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-69850-0_2CrossRefzbMATHGoogle Scholar
  14. 14.
    Fehnker, A., Huuck, R.: Model checking driven static analysis for the real world: designing and tuning large scale bug detection. Innov. Syst. Softw. Eng. 9(1), 45–56 (2013)CrossRefGoogle Scholar
  15. 15.
    Fehnker, A., Huuck, R., Jayet, P., Lussenburg, M., Rauch, F.: Goanna—a static model checker. In: Brim, L., Haverkort, B., Leucker, M., van de Pol, J. (eds.) FMICS 2006. LNCS, vol. 4346, pp. 297–300. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-70952-7_20CrossRefGoogle Scholar
  16. 16.
    Hall, A., Chapman, R.: Correctness by construction: developing a commercial secure system. IEEE Softw. 19(1), 18–25 (2002)CrossRefGoogle Scholar
  17. 17.
    Kinder, J., Katzenbeisser, S., Schallhart, C., Veith, H.: Proactive detection of computer worms using model checking. IEEE Trans. Dependable Secur. Comput. 7(4), 424–438 (2010)CrossRefGoogle Scholar
  18. 18.
    Knudsen, L.R., Leander, G.: PRESENT-block cipher. In: van Tilborg, H.C.A., Jajodia, S. (eds.)Encyclopedia of Cryptography and Security, pp. 953–955. Springer, Boston (2011).  https://doi.org/10.1007/978-1-4419-5906-5
  19. 19.
    Kourie, D.G., Watson, B.W.: The Correctness-by-Construction Approach to Programming. Springer Science & Business Media, Berlin (2012)CrossRefGoogle Scholar
  20. 20.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_47CrossRefGoogle Scholar
  21. 21.
    Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-16612-9_11CrossRefGoogle Scholar
  22. 22.
    Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: ACM SIGPLAN Notices, vol. 41, pp. 42–54. ACM (2006)Google Scholar
  23. 23.
    Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363 (2009)MathSciNetCrossRefGoogle Scholar
  24. 24.
    Mavridou, A., Baranov, E., Bliudze, S., Sifakis, J.: Configuration logics: modeling architecture styles. J. Log. Algebr. Methods Program. 86(1), 2–29 (2017)MathSciNetCrossRefGoogle Scholar
  25. 25.
    National Institute of Standards and Technology. Advanced Encryption Standard. Federal Information Processing Standards Publication, 197 (2001)Google Scholar
  26. 26.
    Osvik, D.A., Shamir, A., Tromer, E.: Cache attacks and countermeasures: the case of AES. In: Pointcheval, D. (ed.) CT-RSA 2006. LNCS, vol. 3860, pp. 1–20. Springer, Heidelberg (2006).  https://doi.org/10.1007/11605805_1CrossRefGoogle Scholar
  27. 27.
    Sutton, J., Carré, B.: Ada: the cheapest way to build a line of business. In: Proceedings of the Conference on TRI-Ada 1995: Ada’s Role in Global Markets: Solutions for a Changing Complex World, pp. 320–330. ACM (1995)Google Scholar
  28. 28.
    Sutton, J., Carré, B.: Achieving high integrity at low cost: a constructive approach. Microprocess. Microsyst. 20(8), 455–461 (1997)CrossRefGoogle Scholar
  29. 29.
    Taft, S., Duff, R., Brukardt, R., Ploedereder, E., Leroy, P., Ada 2012 reference manual. Language and Standard Libraries-International Standard ISO/IEC 8652 (2012)Google Scholar
  30. 30.
    ter Beek, M.H., Carmona, J., Hennicker, R., Kleijn, J.: Communication requirements for team automata. In: Jacquet, J.-M., Massink, M. (eds.) COORDINATION 2017. LNCS, vol. 10319, pp. 256–277. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-59746-1_14CrossRefGoogle Scholar
  31. 31.
    ter Beek, M.H., Carmona, J., Kleijn, J.: Conditions for compatibility of components. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part I. LNCS, vol. 9952, pp. 784–805. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47166-2_55CrossRefGoogle Scholar
  32. 32.
    Tromer, E., Osvik, D.A., Shamir, A.: Efficient cache attacks on AES, and countermeasures. J. Cryptol. 23(1), 37–71 (2010)MathSciNetCrossRefGoogle Scholar
  33. 33.
    Watson, B.W., Kourie, D.G., Cleophas, L.: Experience with correctness-by-construction. Sci. Comput. Program. 97, 55–58 (2015)CrossRefGoogle Scholar
  34. 34.
    Yamane, S., Konoshita, R., Kato, T.: Model checking of embedded assembly program based on simulation. IEICE Trans. Inf. Syst. 100(8), 1819–1826 (2017)CrossRefGoogle Scholar
  35. 35.
    Yang, L., Wang, M., Qiao, S.: Side channel cube attack on PRESENT. In: Garay, J.A., Miyaji, A., Otsuka, A. (eds.) CANS 2009. LNCS, vol. 5888, pp. 379–391. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-10433-6_25CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.InriaRennesFrance

Personalised recommendations