Detail publikace

A Concept of Automated Vulnerability Search in Contactless Communication Applications

Originální název

A Concept of Automated Vulnerability Search in Contactless Communication Applications

Anglický název

A Concept of Automated Vulnerability Search in Contactless Communication Applications

Jazyk

en

Originální abstrakt

Designing and implementing secure applications which use contactless communication link is difficult even when secure hardware is used. Many current proximity devices, such as contactless smart cards or near field communication devices, are verified to be highly secure; however, inappropriate protocol implementation may result in the leak of sensitive information, even if the protocol is also secure by itself. In this paper we show a concept of automated vulnerability search in protocol implementation by using verification methods, which should help developers to verify their applications. We also show simple example of possible attack on seemingly secure payment protocol implemented using seemingly secure smart card to show the way the adversary can abuse improper implementation. The vulnerability the attacker exploits can be in one command or in a combination of commands, which are not vulnerable individually. It is not easy to find such combinations manually, this is where the automated verification methods are put to use. A model checker, provided with an appropriate model, can automatically find vulnerabilities which are not likely to be found manually. The model can be created by the actual communication analysis. We wanted to show that the adversary does not have to have the access to the source code of the application to perform a successful attack, so a platform for the application analysis from the actual contactless communication was developed. The platform provides eavesdropping, altering data for man-in-the-middle attack, and emulating of both communication parties. The source code can help the analysis, but would not be sufficient by itself, so creating model from source code was left for future research. When the model checker finds vulnerability, an attack can be executed. The attack can be either successful, revealing real vulnerability which must be fixed, or unsuccessful, which would result in the model refinement and another model checker run.

Anglický abstrakt

Designing and implementing secure applications which use contactless communication link is difficult even when secure hardware is used. Many current proximity devices, such as contactless smart cards or near field communication devices, are verified to be highly secure; however, inappropriate protocol implementation may result in the leak of sensitive information, even if the protocol is also secure by itself. In this paper we show a concept of automated vulnerability search in protocol implementation by using verification methods, which should help developers to verify their applications. We also show simple example of possible attack on seemingly secure payment protocol implemented using seemingly secure smart card to show the way the adversary can abuse improper implementation. The vulnerability the attacker exploits can be in one command or in a combination of commands, which are not vulnerable individually. It is not easy to find such combinations manually, this is where the automated verification methods are put to use. A model checker, provided with an appropriate model, can automatically find vulnerabilities which are not likely to be found manually. The model can be created by the actual communication analysis. We wanted to show that the adversary does not have to have the access to the source code of the application to perform a successful attack, so a platform for the application analysis from the actual contactless communication was developed. The platform provides eavesdropping, altering data for man-in-the-middle attack, and emulating of both communication parties. The source code can help the analysis, but would not be sufficient by itself, so creating model from source code was left for future research. When the model checker finds vulnerability, an attack can be executed. The attack can be either successful, revealing real vulnerability which must be fixed, or unsuccessful, which would result in the model refinement and another model checker run.

BibTex


@inproceedings{BUT96971,
  author="Martin {Henzl} and Petr {Hanáček} and Peter {Jurnečka} and Matej {Kačic}",
  title="A Concept of Automated Vulnerability Search in Contactless Communication Applications",
  annote="Designing and implementing secure applications which use contactless
communication link is difficult even when secure hardware is used. Many current
proximity devices, such as contactless smart cards or near field communication
devices, are verified to be highly secure; however, inappropriate protocol
implementation may result in the leak of sensitive information, even if the
protocol is also secure by itself. In this paper we show a concept of automated
vulnerability search in protocol implementation by using verification methods,
which should help developers to verify their applications. We also show simple
example of possible attack on seemingly secure payment protocol implemented using
seemingly secure smart card to show the way the adversary can abuse improper
implementation. The vulnerability the attacker exploits can be in one command or
in a combination of commands, which are not vulnerable individually. It is not
easy to find such combinations manually, this is where the automated verification
methods are put to use. A model checker, provided with an appropriate model, can
automatically find vulnerabilities which are not likely to be found manually. The
model can be created by the actual communication analysis. We wanted to show that
the adversary does not have to have the access to the source code of the
application to perform a successful attack, so a platform for the application
analysis from the actual contactless communication was developed. The platform
provides eavesdropping, altering data for man-in-the-middle attack, and emulating
of both communication parties. The source code can help the analysis, but would
not be sufficient by itself, so creating model from source code was left for
future research. When the model checker finds vulnerability, an attack can be
executed. The attack can be either successful, revealing real vulnerability which
must be fixed, or unsuccessful, which would result in the model refinement and
another model checker run.",
  address="Institute of Electrical and Electronics Engineers",
  booktitle="Proceedings 46th Annual IEEE International Carnahan Conference on Security Technology",
  chapter="96971",
  edition="NEUVEDEN",
  howpublished="print",
  institution="Institute of Electrical and Electronics Engineers",
  year="2012",
  month="october",
  pages="180--186",
  publisher="Institute of Electrical and Electronics Engineers",
  type="conference paper"
}