Open APIs for Embedded Security

  • Carl A. Gunter
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2743)


Embedded computer control is increasingly common in appliances, vehicles, communication devices, medical instruments, and many other systems. Some embedded computer systems enable users to obtain their own programs from parties other than the maker of the device. For instance, PDAs and some cell phones offer an open application programming interface that enables users to better customize devices to their needs and support an industry of independent software vendors. This kind of flexibility will be more difficult for other kinds of embedded devices where safety and security are a greater risk. This paper discusses some of the challenges and architectural options for open APIs for embedded systems. These issues are illustrated through an approach to implementing secure programmable payment cards.


Remote Control Smart Card Application Program Interface Payment Card Provider Application 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Grosu, R., Wang, B.-Y.: Automated refinement checking for asynchronous processes. In: 3rd International Conference on Formal Methods in Computer-Aided Design (2000)Google Scholar
  2. 2.
    Alur, R., Wang, B.-Y.: Verifying network protocol implementations by symbolic refinement checking. In: 13th International Conference on Computer- Aided Verification (2001)Google Scholar
  3. 3.
    Bella, G., Massacci, F., Paulson, L.C.: The verification of an industrial payment protocol. In: Atluri, V. (ed.) Proceedings of the 9th ACM Conference on Computer and Communications Security, Washington, DC, ACM Press, New York (2002)Google Scholar
  4. 4.
    Bhargavan, K., Gunter, C.A.: Requirements for a network event recognition language. Electronic Notes in Theoretical Computer Science, vol. 70(4) (December 2002)Google Scholar
  5. 5.
    Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Sax, J.B.: Extended static checking. Research Report 159, Compaq Systems Research Center (1998)Google Scholar
  6. 6.
    Evans, D., Schmalensee, R.I.: Paying with Plastic. MIT Press, Cambridge (1999)Google Scholar
  7. 7.
    Goodloe, A., McDougall, M., Alur, R., Gunter, C.A.: Predictable programs in barcodes. In: Jerraya, A., Wolf, W. (eds.) Proceedings of CASES 2003 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, Grenoble, France, pp. 298–303. ACM Press, New York (2002)Google Scholar
  8. 8.
    Grimaud, G., Lanet, J.-L., Vandewalle, J.-J.: FACADE: A typed intermediate language dedicated to smart cards. In: Nierstrasz, O., Lemoine, M. (eds.) ESEC 1999 and ESEC-FSE 1999. LNCS, vol. 1687, pp. 476–493. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  9. 9.
    Gunter, C.A.: Micro mobile programs. In: Baeza-Yates, R., Montanari, U., Santoro, N. (eds.) Foundations of Information Technology in the Era of Network and Mobile Computing, Montreal, Canada, August 2002, pp. 356–369 (2002); IFIP 17th World Computer Congress — TC1 Stream / International Conference on Theoretical Computer Science (TCS 2002). Kluwer, Dordrecht (2002)Google Scholar
  10. 10.
    Nelson, G., Rustan, K., Leino, M., Saxe, J.B.: ESC/java user’s manual. Technical Note 2000-002, Compaq Systems Research Center (October 2000)Google Scholar
  11. 11.
    Leroy, X.: Bytecode verification for Java smart card. Software Practice & Experience 32, 319–340 (2002)zbMATHCrossRefGoogle Scholar
  12. 12.
    Lyubich, M.: Eine SET Kundembörse mit der Java Card Unterstützung. In: GI Informatiktage 2000. Konradin-Verlag (November 2000)Google Scholar
  13. 13.
    Lyubich, M.: Die architekturen von SET mit der Java Card. In: Bode, A., Karl, W. (eds.) ITG Fachbericht, APC 2001 Arbeitsplatzcomputer (2001)Google Scholar
  14. 14.
    Lyubich, M., Cap, C.: Eine implementierung von SET für Java. In: Tagesband Netzinfrustruckhur und Anwendugen für Informationsgesellschaft, pp. 208–214. Dr. Wilke Verlag (1998)Google Scholar
  15. 15.
    Lyubich, M.: Architectural Concepts for Java Card Running a Payment Protocol and Their Application in a SET Wallet. PhD thesis, University of Rostock (2003)Google Scholar
  16. 16.
    Mastercard and Visa. SET Secure Electronic Transaction Specification: Business Description (May 1997)Google Scholar
  17. 17.
    Mastercard and Visa. SET Secure Electronic Transaction Specification: External Interface Guide (May 1997)Google Scholar
  18. 18.
    Mastercard and Visa. SET Secure Electronic Transaction Specification: Formal Protocol Definition (May 1997)Google Scholar
  19. 19.
    Mastercard and Visa. SET Secure Electronic Transaction Specification: Programmer’s Guide (May 1997)Google Scholar
  20. 20.
    Rose, E., Rose, K.H.: Lightweight bytecode verification. In: Workshop “Formal Underpinnings of the Java Paradigm”, OOPSLA 1998 (1998)Google Scholar
  21. 21.
    Schneider, F.B.: Enforceable security policies. ACM Transactions on Information and System Security 3, 30–50 (2000)CrossRefGoogle Scholar
  22. 22.
    Schneier, B.: Secrets and Lies. John Wiley & Sons, Chichester (2000)Google Scholar
  23. 23.
    Sun Microsystems. Java 2 Platform Icro Edition (J2ME) Technology for Creating Mobile Devices (May 2000). White paper,
  24. 24.
    van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 299–312. Springer, Heidelberg (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Carl A. Gunter
    • 1
  1. 1.Department of Computer and Information ScienceUniversity of PennsylvaniaPhiladelphia

Personalised recommendations