User Tools
security-by-contract_for_mobile_and_smart_card
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
security-by-contract_for_mobile_and_smart_card [2013/03/25 14:04] olga.gadyatskaya@unitn.it [Security-by-Contract for Mobiles and Smart Cards] |
security-by-contract_for_mobile_and_smart_card [2021/01/29 10:58] (current) |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Security-by-Contract for Mobiles and Smart Cards ====== | ====== Security-by-Contract for Mobiles and Smart Cards ====== | ||
| - | Among the [[research_activities|research topics]] of the [[start|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). | + | Among the [[research_activities|research topics]] of the [[start|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. | ||
| + | |||
| + | ==== Themes ==== | ||
| + | |||
| + | 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 | ||
| - | 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 are 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 [[http://www.cs.kuleuven.be/~frank|Frank Piessens]] from KUL. | 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 [[http://www.cs.kuleuven.be/~frank|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 SIM card open for over-the-air application loading). | + | 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: ({{:research_activities:security-by-contract_for_mobile_and_smart_card:sxc-short-paper.pdf|Whitepaper PDF}}, [[http://disi.unitn.it/~gadyatskaya/sxc.html|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. | A short description of the embedded checker for smart cards can be found here: ({{:research_activities:security-by-contract_for_mobile_and_smart_card:sxc-short-paper.pdf|Whitepaper PDF}}, [[http://disi.unitn.it/~gadyatskaya/sxc.html|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. | ||
| Line 16: | Line 25: | ||
| - | 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. More details of our proposal can be found here: [[http://disi.unitn.it/~gadyatskaya/osgi.html|SxC for OSGi]]. | + | 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: [[http://disi.unitn.it/~gadyatskaya/osgi.html|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. | 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. | ||
| - | ==== Themes ==== | ||
| - | |||
| - | 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 | ||
| ==== People ==== | ==== People ==== | ||
| Line 33: | Line 35: | ||
| * Nicola Dragoni | * Nicola Dragoni | ||
| - | * Olga Gadyatskaya | + | * Olga Gadyatskaya (active) |
| * Ida Siahaan | * Ida Siahaan | ||
| - | * Nicola La Torre | + | * Marco De La Torre |
| - | * Fabio Massacci | + | * Fabio Massacci (active) |
| - | * Katsyarina Naliuka | + | * Katsyarina Naliuka |
| + | * Anton Philippov (active) | ||
| ==== Projects ==== | ==== Projects ==== | ||
| Line 45: | Line 48: | ||
| * [[SECURECHANGE]] | * [[SECURECHANGE]] | ||
| * [[S3MS]] | * [[S3MS]] | ||
| + | * [[NESSOS]] | ||
| ====Talks and Tutorials ==== | ====Talks and Tutorials ==== | ||
| Line 57: | Line 60: | ||
| ==== Publications ==== | ==== Publications ==== | ||
| **SxC for Java Card:** | **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 {{:research_activities:security-by-contract_for_mobile_and_smart_card:gady-mass-hats2012.pdf|PDF}} | ||
| * O.Gadyatskaya, F.Massacci and E.Lostal: // Extended Abstract: Embeddable Security-by-Contract Verifier for Java Card. // In BYTECODE-2012, Tallinn, Estonia, 2012. {{:research_activities:security-by-contract_for_mobile_and_smart_card:gady-mass-lost-bytecode-2012.pdf|PDF}} | * O.Gadyatskaya, F.Massacci and E.Lostal: // Extended Abstract: Embeddable Security-by-Contract Verifier for Java Card. // In BYTECODE-2012, Tallinn, Estonia, 2012. {{:research_activities:security-by-contract_for_mobile_and_smart_card:gady-mass-lost-bytecode-2012.pdf|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.{{:research_activities:security-by-contract_for_mobile_and_smart_card:gady-mass-lost-iciss-2011.pdf|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.{{:research_activities:security-by-contract_for_mobile_and_smart_card:gady-mass-lost-iciss-2011.pdf|PDF}} | ||
| Line 88: | Line 91: | ||
| ==== Software ==== | ==== Software ==== | ||
| - | * 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 Gadyatskaya[[name.surname@unitn.it]] | + | * 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 Gadyatskaya[[name.surname@unitn.it]] |
security-by-contract_for_mobile_and_smart_card.1364216692.txt.gz · Last modified: 2021/01/29 10:58 (external edit)
Page Tools
