|
 ABSTRACT
We motivate the design of typed assembly language (TAL) and present a type-preserving ttranslation from Systemn F to TAL. The typed assembly language we pressent is based on a conventional RISC assembly language, but its static type sytem provides support for enforcing high-level language abstratctions, such as closures, tuples, and user-defined abstract data types. The type system ensures that well-typed programs cannot violatet these abstractionsl In addition, the typing constructs admit many low-level compiler optimiztaions. Our translation to TAL is specified as a sequence of type-preserving transformations, including CPS and closure conversion phases; type-correct source programs are mapped to type-correct assembly language. A key contribution is an approach to polymorphic closure conversion that is considerably simpler than previous work. The compiler and typed assembly lanugage provide a fully automatic way to produce certified code, suitable for use in systems where unstrusted and potentially malicious code must be checked for safety before execution.
REFERENCES
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.
| |
1
|
|
| |
2
|
APPEL, A. W. AND MACQUEEN, D. B. 1991. Standard ML of New Jersey. In 3rd International Symposium on Programming Language Implementation and Logic Programming, M. Wirsing, Ed. Springer-Verlag, New York, NY, USA, 1-13. Volume 528 of Lecture Notes in Computer Science.
|
 |
3
|
B. N. Bershad , S. Savage , P. Pardyak , E. G. Sirer , M. E. Fiuczynski , D. Becker , C. Chambers , S. Eggers, Extensibility safety and performance in the SPIN operating system, Proceedings of the fifteenth ACM symposium on Operating systems principles, p.267-283, December 03-06, 1995, Copper Mountain, Colorado, United States
|
| |
4
|
BIRKEDAL, L., ROTHWELL, N., TOFTE, M., AND TURNER, D. 1993. The ML Kit (version 1). Tech. Rep. 93//14, Department of Computer Science, University of Copenhagen.
|
| |
5
|
|
| |
6
|
|
| |
7
|
Karl Crary , Stephanie Weirich , Greg Morrisett, Intensional polymorphism in type-erasure semantics, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.301-312, September 26-29, 1998, Baltimore, Maryland, United States
|
| |
8
|
DANVY, O. AND FILINSKI, A. 1992. Representing control: a study of the CPS transformation. Math. Struct. Comput. Sci. 2, 4 (Dec.), 361-391.
|
| |
9
|
Allyn Dimock , Robert Muller , Franklyn Turbak , J. B. Wells, Strongly typed flow-directed representation transformations (extended abstract), Proceedings of the second ACM SIGPLAN international conference on Functional programming, p.11-24, June 09-11, 1997, Amsterdam, The Netherlands
|
| |
10
|
GIRARD, J.-Y. 1971. Une extension de l'interpr6tation de GSdel 5~ l'analyse, et son application 5~ l'61imination de coupures dans l'analyse et la th6orie des types. In Proceedings of the Second Scandinavian Logic Symposium, J. E. Fenstad, Ed. North-Holland, 63-92.
|
| |
11
|
GIRARD, J.-Y. 1972. Interpr6tation fonctionelle et 61imination des coupures de l'arithm6tique d'ordre sup6rieur. Ph.D. thesis, Universit6 Paris VII.
|
| |
12
|
|
| |
13
|
|
| |
14
|
|
| |
15
|
|
| |
16
|
INTEL. 1996. Intel Architecture Software Developer's Manual. Intel Corporation, P.O. Box 7641, Mt. Prospect IL 60056-7641.
|
| |
17
|
David Kranz , Norman Adams , Richard Kelsey , Jonathan Rees , Paul Hudak , James Philbin, ORBIT: an optimizing compiler for scheme, Proceedings of the 1986 SIGPLAN symposium on Compiler construction, p.219-233, June 25-27, 1986, Palo Alto, California, United States
|
| |
18
|
|
| |
19
|
|
| |
20
|
|
| |
21
|
|
| |
22
|
Yasuhiko Minamide , Greg Morrisett , Robert Harper, Typed closure conversion, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.271-283, January 21-24, 1996, St. Petersburg Beach, Florida, United States
[doi> 10.1145/237721.237791]
|
| |
23
|
|
| |
24
|
MORRISETT, G., CRARY, K., GLEW, N., GROSSMAN, D., SAMUELS, R., SMITH, F., WALKER, D., WEIRICH, S., AND ZDANCEWlC, S. 1999. TALx86: A realistic typed assembly language. In ACM SIGPLAN Workshop on Compiler Support for System Software. INRIA Research Report, vol. 0228. INRIA, Centre de Diffusion, INRIA, BP 105-78153 Le Chesnay Cedex, France.
|
| |
25
|
|
| |
26
|
|
| |
27
|
MORRISETT, G., TARDITI, D., CHENG, P., STONE, C., HARPER, R., AND LEE, P. 1996. The TIL/ML compiler: Performance and safety through types. In ACM SIGPLAN Workshop on Compiler Support for System Software.
|
| |
28
|
|
| |
29
|
|
| |
30
|
|
| |
31
|
PEYTON JONES, S., HALL, C., HAMMOND, K., PARTAIN, W., AND WADLER, P. 1993. The Glasgow Haskell compiler: a technical overview. In Proc. UK Joint Framework for Information Technology (JFIT) Technical Conference. 249-257.
|
| |
32
|
|
| |
33
|
SHAO, Z. 1997. An overview of the FLINT/ML compiler. In Workshop on Types in Compilation. Boston College Computer Science Department Technical Report, vol. BCSS-97-03. Boston College, Fulton Hall, Room 460, Chestnull Hill, MA 02467-3808, USA.
|
| |
34
|
STEELE, JR., G. 1978. Rabbit: A compiler for Scheme. M.S. thesis, MIT.
|
| |
35
|
D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, United States
|
| |
36
|
|
| |
37
|
|
| |
38
|
WADLER, P. 1990b. Linear types can change the world! In Programming Concepts and Methods, M. Broy and C. Jones, Eds. North-Holland, Sea of Galilee, Israel. IFIP TC 2 Working Conference.
|
| |
39
|
|
| |
40
|
|
| |
41
|
|
| |
42
|
|
| |
43
|
|
CITED BY 122
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Christopher Colby , Peter Lee , George C. Necula , Fred Blau , Mark Plesko , Kenneth Cline, A certifying compiler for Java, ACM SIGPLAN Notices, v.35 n.5, p.95-107, May 2000
|
|
|
|
|
|
|
|
|
Jeffery von Ronne , Andreas Hartmann , Wolfram Amme , Michael Franz, Efficient online optimization by utilizing offline analysis and the safeTSA representation, Proceedings of the inaugural conference on the Principles and Practice of programming, 2002 and Proceedings of the second workshop on Intermediate representation engineering for virtual machines, 2002, June 13-14, 2002, Dublin, Ireland
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Yao-Wen Huang , Fang Yu , Christian Hang , Chung-Hung Tsai , Der-Tsai Lee , Sy-Yen Kuo, Securing web application code by static analysis and runtime protection, Proceedings of the 13th international conference on World Wide Web, May 17-20, 2004, New York, NY, USA
|
|
|
David Tarditi , Greg Morrisett , Perry Cheng , Chris Stone , Robert Harper , Peter Lee, TIL: a type-directed, optimizing compiler for ML, ACM SIGPLAN Notices, v.39 n.4, April 2004
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Bor-Yuh Evan Chang , Adam Chlipala , George C. Necula , Robert R. Schneck, Type-based verification of sssembly language for compiler debugging, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.91-102, January 10-10, 2005, Long Beach, California, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Manuel V. Hermenegildo , Elvira Albert , Pedro López-García , Germán Puebla, Abstraction carrying code and resource-awareness, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.1-11, July 11-13, 2005, Lisbon, Portugal
|
|
|
|
|
|
Vijay S. Menon , Neal Glew , Brian R. Murphy , Andrew McCreight , Tatiana Shpeisman , Ali-Reza Adl-Tabatabai , Leaf Petersen, A verifiable SSA program representation for aggressive compiler optimization, ACM SIGPLAN Notices, v.41 n.1, p.397-408, January 2006
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Mark Aiken , Manuel Fähndrich , Chris Hawblitzel , Galen Hunt , James Larus, Deconstructing process isolation, Proceedings of the 2006 workshop on Memory system performance and correctness, October 22-22, 2006, San Jose, California
|
|
|
Gary T. Leavens , Jean-Raymond Abrial , Don Batory , Michael Butler , Alessandro Coglio , Kathi Fisler , Eric Hehner , Cliff Jones , Dale Miller , Simon Peyton-Jones , Murali Sitaraman , Douglas R. Smith , Aaron Stump, Roadmap for enhanced languages and methods to aid verification, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Chris Hawblitzel , Heng Huang , Lea Wittie , Juan Chen, A garbage-collecting typed assembly language, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
David Swasey , Tom Murphy, VII , Karl Crary , Robert Harper, A separate compilation extension to standard ML, Proceedings of the 2006 workshop on ML, September 16-16, 2006, Portland, Oregon, USA
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Galen Hunt , Mark Aiken , Manuel Fähndrich , Chris Hawblitzel , Orion Hodson , James Larus , Steven Levi , Bjarne Steensgaard , David Tarditi , Ted Wobber, Sealing OS processes to improve dependability and safety, ACM SIGOPS Operating Systems Review, v.41 n.3, June 2007
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Jeremy Condit , Brian Hackett , Shuvendu K. Lahiri , Shaz Qadeer, Unifying type checking and property checking for low-level code, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
|
|
|
|
|
|
|
|
|
|
INDEX TERMS
Primary Classification:
D.
Software
D.3
PROGRAMMING LANGUAGES
D.3.2
Language Classifications
Subjects:
Macro and assembly languages
Additional Classification:
D.
Software
D.2
SOFTWARE ENGINEERING
D.2.11
Software Architectures
Subjects:
Languages (e.g., description, interconnection, definition)
D.3
PROGRAMMING LANGUAGES
D.3.1
Formal Definitions and Theory
Subjects:
Semantics;
Syntax
D.3.4
Processors
Subjects:
Compilers
F.
Theory of Computation
F.3
LOGICS AND MEANINGS OF PROGRAMS
F.3.2
Semantics of Programming Languages
Subjects:
Operational semantics
F.3.3
Studies of Program Constructs
Subjects:
Type structure
General Terms:
Languages,
Security,
Theory,
Verification
Keywords:
certified code,
closure conversion,
secure extensible systems,
type-directed compilation,
typed assembly language,
typed intermediate languages
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf