Compiling C Programs into a Strongly Typed Assembly Language

  • Takahiro Kosakai
  • Toshiyuki Maeda
  • Akinori Yonezawa
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4846)


C is one of the most popular languages in system programming, though its unsafe nature often causes security vulnerabilities. In the face of this situation, many tools are developed to ensure safety properties of C programs. However, most of them work at the source code level, and conventional compilers lose safety guarantee as they translate source code into assembly code. In this paper, we present CTAL0, a strongly typed assembly language that is aimed at certifying the memory safety of assembly code compiled from C programs. CTAL0 is expressive enough to implement potentially unsafe ANSI C features including pointer arithmetics and casts. We have also implemented a type-checker and an experimental C compiler that produces safe CTAL0 assembly code by performing several transformations on given programs to avoid dangerous operations.


typed assembly language memory safety 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Kernighan, B.W., Ritchie, D.M.: The C Programming Language, 2nd edn. Prentice-Hall, Englewood Cliffs (1988)Google Scholar
  2. 2.
    SecurityFocus: SecurityFocus vulnerability database,
  3. 3.
    Necula, G.C., Condit, J., Harren, M., McPeak, S., Weimer, W.: CCured: Type-safe retrofitting of legacy software. ACM Transactions on Programming Languages and Systems 27(3), 477–526 (2005)CrossRefGoogle Scholar
  4. 4.
    Oiwa, Y., Sekiguchi, T., Sumii, E., Yonezawa, A.: Fail-safe ANSI-C compiler: An approach to making C programs secure (progress report). In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol. 2609, pp. 133–153. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    Morrisett, G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. In: Proc. of POPL, pp. 85–97 (1998)Google Scholar
  6. 6.
    Xi, H., Harper, R.: A dependently typed assembly language. In: Proc. of ICFP, pp. 169–180 (2001)Google Scholar
  7. 7.
    Morrisett, G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. In: Leroy, X., Ohori, A. (eds.) TIC 1998. LNCS, vol. 1473, pp. 28–52. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  8. 8.
    Walker, D., Morrisett, G.: Alias types for recursive data structures. In: Harper, R. (ed.) TIC 2000. LNCS, vol. 2071, pp. 177–206. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  9. 9.
    Maeda, T., Yonezawa, A.: Writing practical memory management code with a strictly typed assembly language. In: Proc. of SPACE (2006)Google Scholar
  10. 10.
    Intel Corporation: Intel 64 and IA-32 architectures software developer’s manual (2006)Google Scholar
  11. 11.
    Turner, D.N., Wadler, P., Mossin, C.: Once upon a type. In: Proc. of FPCA, pp. 1–11 (1995)Google Scholar
  12. 12.
    Kosakai, T.: CTALo implementations distribution site,
  13. 13.
    Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)Google Scholar
  14. 14.
    Free Software Foundation: The GNU compiler collection,
  15. 15.
    Zhou, F., Condit, J., Anderson, Z., Bagrak, I., Ennals, R., Harren, M., Necula, G., Brewer, E.: SafeDrive: Safe and recoverable extensions using language-based techniques. In: Proc. of OSDI, pp. 45–60 (2006)Google Scholar
  16. 16.
    Condit, J., Harren, M., Anderson, Z., Gay, D., Necula, G.C.: Dependent types for low-level programming. In: Proc. of ESOP (2007)Google Scholar
  17. 17.
    Jim, T., Morrisett, G., Grossman, D., Hicks, M., Cheney, J., Wang, Y.: Cyclone: A safe dialect of C. In: Proc. of USENIX ATC, pp. 275–288 (2002)Google Scholar
  18. 18.
    Morrisett, G., Crary, K., Glew, N., Grossman, D., Samuels, R., Smith, F., Walker, D., Weirich, S., Zdancewic, S.: TALx86: A realistic typed assembly language. In: Proc. of WCSSS, Atlanta, GA, USA, May 1999, pp. 25–35 (1999)Google Scholar
  19. 19.
    Harren, M., Necula, G.C.: Using dependent types to certify the safety of assembly code. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 155–170. Springer, Heidelberg (2005)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Takahiro Kosakai
    • 1
  • Toshiyuki Maeda
    • 1
  • Akinori Yonezawa
    • 1
  1. 1.Department of Computer Science, Graduate School of Information Science and Technology, The University of Tokyo, 7-3-1 Hongo, Bunkyo-ku, TokyoJapan

Personalised recommendations