Skip to main content
SpringerLink
Log in

More Typed Assembly Languages for Confidentiality

  • Conference paper
Programming Languages and Systems (APLAS 2007)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4807))

Included in the following conference series:

Abstract

We propose a series of type systems for the information-flow security of assembly code. These systems extend previous work TAL C with some timing annotations and associated judgments and rules. By using different timing rules, these systems are applicable to different practical settings. In particular, they can be used to prevent illicit information flow through the termination and timing channels in sequential programs as well as the possibilistic and probabilistic channels in multi-threaded programs. We present the formal details of these as a generic type system TAL\(^+_{C}\) and prove its noninterference. TAL\(^+_{C}\) is designed as a core target language for certifying compilation. We illustrate its use with a formal scheme of type-preserving translation.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Agat, J.: Transforming out timing leaks. In: Proc. 27th ACM Symposium on Principles of Programming Languages, Boston, MA, pp. 40–53 (January 2000)

    Google Scholar 

  2. Agat, J.: Type-based techniques for covert channel elimination and register allocation. PhD thesis, Chalmers Univ. of Technology & Gothenburg Univ. Gothenburg, Sweden (December 2000)

    Google Scholar 

  3. Ball, T.: What’s in a region? Or computing control dependence regions in near-linear time for reducible control flow. ACM Letters on Prog. Lang. & Syst. 2(1–4), 1–16 (1993)

    Article  Google Scholar 

  4. Barthe, G., Basu, A., Rezk, T.: Security types preserving compilation. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 2–15. Springer, Heidelberg (2004)

    Google Scholar 

  5. Barthe, G., Naumann, D., Rezk, T.: Deriving an information flow checker and certifying compiler for Java. In: Proc. 2006 IEEE Symposium on Security and Privacy, Oakland, CA, pp. 230–242 (May 2006)

    Google Scholar 

  6. Barthe, G., Rezk, T., Russo, A., Sabelfeld, A.: Security of multithreaded programs by compilation. In: ESORICS 2007. LNCS, vol. 4734, Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  7. Crary, K., Weirich, S.: Resource bound certification. In: Proc. 27th ACM symposium on Principles of programming languages, Boston, MA, USA, pp. 184–198 (January 2000)

    Google Scholar 

  8. Hedin, D., Sands, D.: Timing aware information flow security for a JavaCard-like bytecode. In: Proc. 1st Workshop on Bytecode Semantics, Verification, Analysis and Transformation, Edinburgh, Scotland, UK, pp. 163–182 (April 2005)

    Google Scholar 

  9. Kobayashi, N., Shirane, K.: Type-based information flow analysis for low-level languages. In: 3rd Asian Workshop on Prog. Lang. & Syst. Shanghai, China, pp. 302–316 (November 2002)

    Google Scholar 

  10. Kozen, D.: Language-based security. In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 284–298. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  11. Laud, P.: Semantics and program analysis of computationally secure information flow. In: Proc. 10th European Symposium on Programming, Genova, Italy, pp. 77–91 (April, 2001)

    Google Scholar 

  12. Medel, R., Compagnoni, A., Bonelli, E.: A typed assembly language for non-interference. In: Proc. 9th ICTCS, Siena, Italy, pp. 360–374 (October 2005)

    Google Scholar 

  13. Morrisett, G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. ACM Transactions on Programming Languages and Systems 21(3), 527–568 (1999)

    Article  Google Scholar 

  14. Myers, A.C., Liskov, B.: Complete, safe information flow with decentralized labels. In: Proc. IEEE Symposium on Security and Privacy, Oakland, CA, pp. 186–197 (May 1998)

    Google Scholar 

  15. Myers, A.C., et al.: Jif: Java + information flow (2001), http://www.cs.cornell.edu/jif/

  16. Necula, G.C., Lee, P.: Safe, untrusted agents using proof-carrying code. In: Vigna, G. (ed.) Mobile Agents and Security. LNCS, vol. 1419, pp. 61–91. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  17. Pierro, A.D., Hankin, C., Wiklicky, H.: Approximate non-interference. In: Proc. 15th CSFW, Cape Breton, NS, Canada, pp. 1–17 (June 2002)

    Google Scholar 

  18. Sabelfeld, A.: The impact of synchronisation on secure information flow in concurrent programs. In: Bjørner, D., Broy, M., Zamulin, A.V. (eds.) PSI 2001. LNCS, vol. 2244, pp. 227–241. Springer, Heidelberg (2001)

    Google Scholar 

  19. Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)

    Article  Google Scholar 

  20. Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-thread programs. In: CSFW, Cambridge, England, pp. 200–214 (July 2000)

    Google Scholar 

  21. Schneider, F.B., Morrisett, G., Harper, R.: A language-based approach to security. In: Wilhelm, R. (ed.) Informatics. LNCS, vol. 2000, pp. 86–101. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  22. Smith, G.: A new type system for secure information flow. In: CSFW, Cape Breton, NS, Canada, pp. 115–125 (2001)

    Google Scholar 

  23. Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: POPL, San Diego, CA, pp. 355–364 (January 1998)

    Google Scholar 

  24. Vanderwaart, J.C., Crary, K.: Automated and certified conformance to responsiveness policies. In: TLDI, Long Beach, CA, pp. 79–90 (January 2005)

    Google Scholar 

  25. Volpano, D., Smith, G.: Eliminating covert flows with minimum typings. In: CSFW, Rockport, MA, pp. 156–169 (June 1997)

    Google Scholar 

  26. Volpano, D., Smith, G.: A type-based approach to program security. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 607–621. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  27. Volpano, D., Smith, G.: Probabilistic noninterference in a concurrent language. In: CSFW, Rockport, MA, pp. 34–43 (June 1998)

    Google Scholar 

  28. Xi, H., Harper, R.: A dependently typed assembly language. In: Proc. 6th ACM International Conference on Functional Programming, Florence, Italy, pp. 169–180 (September 2001)

    Google Scholar 

  29. Yu, D.: More typed assembly languages for confidentiality. Technical Report DCL-TR-2006-0021, DoCoMo USA Labs, San Jose, CA (September 2006), http://www.docomolabsresearchers-usa.com/~dyu/talcp-tr.pdf

  30. Yu, D., Islam, N.: A typed assembly language for confidentiality. Technical Report DCL-TR-2005-0002, DoCoMo USA Labs, San Jose, CA (March 2005), http://www.docomolabsresearchers-usa.com/~dyu/talc-tr.pdf

  31. Yu, D., Islam, N.: A typed assembly language for confidentiality. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, pp. 162–179. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  32. Zdancewic, S., Myers, A.C.: Robust declassification. In: CSFW, Cape Breton, NS, Canada, pp. 15–23 (June 2001)

    Google Scholar 

  33. Zdancewic, S., Myers, A.C.: Secure information flow via linear continuations. Higher-Order and Symbolic Computation 15(2–3), 209–234 (2002)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DoCoMo Communications Laboratories, USA

    Dachuan Yu

Authors
  1. Dachuan Yu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Zhong Shao

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Yu, D. (2007). More Typed Assembly Languages for Confidentiality. In: Shao, Z. (eds) Programming Languages and Systems. APLAS 2007. Lecture Notes in Computer Science, vol 4807. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76637-7_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-76637-7_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-76636-0

  • Online ISBN: 978-3-540-76637-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation