Security-by-Contract for Mobiles and Smart Cards

Among the research topics of the Security Group we focus here on checking that an application satisfies a security property by running a checker on a mobile phone or even smaller devices. It looks like a doomed enterprise, as everybody knows that static analyzers are slow, memory-hungry and utterly useless for anything but off-line verification of specifications (rarely code). However, we were able to achieve a lot.

Our idea, dubbed the Security-by-Contract approach, is that a checker could verify on the fly whether an application would respect the security policy of a mobile phone application at download time, e.g. you could forbid the possibility of sending silent SMSs or making phone calls to premium numbers. If the application didn’t meet your constraints you would inoculate it with your policy monitoring algorithm. In this way the phone should not trust anybody, no market place, no security ratings, etc. It could just trust itself. Of course you always have the Android's alternative of having the user clicking yes on accepting a Manifest that she doesn't understand, and where the guidelines for developers are to ask all permissions possible, even if you don't need them.

Within the main stream project we covered a number of themes.

• Security for Android phones (ongoing)
• Load-time security checking for Java smart cards
• Load-time checking and run-time monitoring for .NET and Java Phones

In 2006 in the S3MS project we proved it worked on many different mobile phones (Java and .NET) equipped with the system. It was the start of a long standing collaboration with Frank Piessens from KUL.

Recently in the framework of the SECURECHANGE project we were able to push the envelope even further: we could run the verification technique over a smart card by meeting the tough requirements set forth by Gemalto, one of the leading companies in the field. This might be a possible road for the deployment of open, multi-applications smart cards (one of the use cases is a SIM card open for over-the-air application loading).

A short description of the embedded checker for smart cards can be found here: (Whitepaper PDF, Dedicated website). In a nutshell, the checker parses the loaded bytecode and infers the calls to shared services of other applications on card. Each application declares its own access control policy specifying which are the authorized clients per each provided service. On the card this policy is matched against the code of the existing applets; while the loaded code is evaluated with respect to the policies of the existing applets. In this way we ensure already at load time that only authorized clients will be able to invoke the sensitive services. The standard Java Card approach to enforce these kinds of policies is embedding them directly into the application code, what hinders the future application updates and introduces the run-time checking overhead.

The next figure summarizes the load time checking architecture (the white items belong to the standard Java Card architecture, the gray items are introduced by the SxC approach). Our solution is fully backward-compatible with the existing Java Card platforms and requires only minimal changes to the platform Installer and Loader components.

The SxC idea was also applied to multi-tenant OSGi platforms. An application contract (implemented on OSGi as a part of the manifest) was used to enable declarative policies for bundle interactions. We used as a case study a smart home scenario generously shared by Telefonica. More details of our proposal can be found here: SxC for OSGi.

Currently we are researching how to apply the load time checks on Android and other novel mobile platforms. The load time checks are appropriate for mobile platforms: the users typically expect that installation of an app will take some time, while they will not tolerate the delays introduced by run-time monitoring in the execution of their favorite apps. In the same time, during load time we can already effectively disable some vulnerabilities in the app code, such as reducing the number of permissions granted to the app to the permissions actually required in the code.

The following is a list a people that has been involved in the project at some point in time.

• Nicola Dragoni
• Olga Gadyatskaya (active)
• Ida Siahaan
• Marco De La Torre
• Fabio Massacci (active)
• Katsyarina Naliuka
• Anton Philippov (active)

This activity was supported by a number of projects

• SECURECHANGE
• S3MS
• NESSOS

• Fabio Massacci. Load‐Time Security Certification for Real Smart‐Cards. Hasso-Plattner Institute Berlin. February 2011. Slides
• Olga Gadyatskaya, Fabio Massacci. Load‐Time Security Certification for Real Smart‐Cards. Nokia Research Center, January 2011. Slides
• Olga Gadyatskaya The Embeddable Security-by-Contract Verifier for Java Card. BYTECODE-2012 Workshop, March 2012. Slides
• Olga Gadyatskaya, Fabio Massacci Load-Time Security Certification for Real Smart-Cards. FMCO-HATS Summer School Tutorial. September 2012. Slides

SxC for Java Card:

• O.Gadyatskaya and F.Massacci: Controlling Application Interactions on the Novel Smart Cards with Security-by-Contract. In Proceedings of HATS-2012 Summer School, Springer PDF
• O.Gadyatskaya, F.Massacci and E.Lostal: Extended Abstract: Embeddable Security-by-Contract Verifier for Java Card. In BYTECODE-2012, Tallinn, Estonia, 2012. PDF
• O. Gadyatskaya, F. Massacci and E. Lostal: Load Time Security Verification. In Proceedings of International Conference on Information Systems Security (ICISS 2011), Kolkata, India, vol. LNCS 7093 pp. 250-264, Springer.PDF
• N. Dragoni, O. Gadyatskaya and F. Massacci: Supporting Software Evolution for Open Smart Cards by Security-by-Contract. In Petre et al.: Dependability and Computer Engineering: Concepts for Software-Intensive Systems, IGI Global, 2011. PDF available at the IGI Global web site Link
• N. Dragoni, O. Gadyatskaya, F. Massacci, F. Paci and E. Lostal: Loading-Time Verification for Open Multi-Application Smart Cards. In Proceedings of the IEEE International Symposium on Policies for Distributed Systems and Networks (POLICY 2011), Pisa, Italy, 2011, pp. 153-156, IEEE Computer Society. PDF
• O. Gadyatskaya, F. Massacci, F. Paci, S. Stankevich: Java Card Architecture for Autonomous Yet Secure Evolution of Smart Cards Applications. In Proceedings of NordSec 2010, LNCS 7127, pp187-192. Springer 2012. PDF
• N. Dragoni, O. Gadyatskaya and F. Massacci: Supporting Applications' Evolution in Multi-Application Smart Cards by Security-by-Contract. In Proceedings of the 4th Workshop in Information Security Theory and Practices (WISTP 2010), Passau, Germany, 2010, vol. LNCS 6033, pp.221-228, Springer. PDF

SxC for OSGi:

• O. Gadyatskaya, F. Massacci and A. Philippov: Security-by-Contract for the OSGi Platform. In Proceedings of 27th IFIP TC 11 Information Security and Privacy Conference (SEC 2012), Springer 2012 PDF

SxC for Mobile Phones:

• Bielova N., Dragoni N., Massacci N., Naliuka K., Siahaan I.: Matching in security-by-contract for mobile code. Journal of Logic and Algebraic Programming 78(5):340-358, (2009)PDF
• Dragoni N., Massacci F., Walter T., Schaefer C.. What the Heck is this application doing? - A security-by-contract architecture for pervasive services, Computer & Security 28(7):566-577 2009. PDF at Elsevier
• F. Massacci, F. Piessens, I. Siahaan: Security-by-contract for the future internet. Proc. of FIS’09. LNCS 5468. p. 29-43, Springer 2009.PDF
• Desmet L., Joosen W., Massacci F., Naliuka K., Philippaerts P., Piessens F., Vanoverberghe D.. The S3MS.NET Run Time Monitor. Tool Demonstration. ENTCS 253(5):153-159, 2009.
• Aktug I., Naliuka K.: ConSpec — A formal language for policy specification. Science of Computer Programming 74(1–2):2-12, 2008. PDF. PDF at Elsevier
• Desmet L, Joosen W., Massacci F., Philippaerts P., Piessens F., Siahaan I., Vanoverberghe D., Security-by-contract on the .NET platform. Information Security Technical Report 13 (1):25-32, Jan 2008. (most cited paper of the journal) PDF at Elsevier. Short version appeared at ACM CSAW (see below)
• F. Massacci, K. Naliuka: Towards practical security monitors of UML policies for mobile applications. Proc. of ARES Workshops’08. p. 1112-1119, 2008.
• N. Dragoni, F. Massacci, K. Naliuka: An inline monitoring system for .NET mobile devices. Proc. of IFIPTM’08. 363-366, 2008.
• F. Massacci, I. Siahaan. Simulating Midlet’s Security Claims with Automata Modulo Theory. In Proc. of PLAS’08. May 2008 Tucson (USA), p 1-19, ACM Press, 2008.
• L. Desmet, W. Joosen, F. Massacci, K. Naliuka, P. Philippaerts, F. Piessens, D. Vanoverbergh: A flexible security architecture to support third-party applications on mobile devices. In Proc. of CSAW’07. p. 19-28 ACM Press 2007.PDF
• N. Dragoni, F. Massacci: Security-by-contract for web services. In Proc. of SWS’07. p. 90-98 ACM Press 2007.
• N. Dragoni, F. Massacci, K. Naliuka, I. Siahaan: Security-by-Contract: Toward a Semantics for Digital Signatures on Mobile Code. In Proc. of EuroPKI 2007. LNCS, 4582, p. 297-312 Springer, 2007.PDF
• N. Dragoni, F. Massacci, C. Schaefer, T. Walter, E. Vetillard. A Security-by-Contracts Architecture for Pervasive Services. In Proc. of SecPerU’07. p 49 – 54, IEEE Press 2007.
• F. Massacci, K. Naliuka: Towards Practical Security Monitors of UML Policies for Mobile Applications. In Proc. of Policy 2007, p. 278-278. , IEEE Press.
• F. Massacci, I. Siahaan. Matching Midlet's Security Claims with a Platform Security Policy using Automata Modulo Theory. In Proc. of NordSec’07. 2007. PDF

• We released the binaries of the SxC verifier for Java Card (the developer version for PC). To get them please contact Fabio Massacci or Olga Gadyatskayaname.surname@unitn.it