Among the research topics of the Security Group we focus on here on checking that an application satisfies a security property by running a checker on a mobile phone or even smaller devices. It looks 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).

Our idea 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 Android's alternative of having the user clicking yes on accepting a Manifest that it doesn't understand and where the guidelines for developers is to ask all permissions possible, even if you don't need them.

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. A short description of the embedded checker for smart cards can be found here: (Short PDF, Dedicated website).

The SxC idea was also applied to multi-tenant OSGi platforms. An application contract (implemented on OSGi as 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.

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

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

• Nicola Dragoni
• Olga Gadyatskaya
• Ida Siahaan
• Nicola La Torre
• Fabio Massacci
• Katsyarina Naliuka

This activity was supported by a number of projects

• SECURECHANGE
• S3MS

• 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, 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