Toward a foundational typed assembly language

Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '03 ◽

10.1145/604131.604149 ◽

2003 ◽

Cited By ~ 27

Author(s):

Karl Crary

Keyword(s):

Assembly Language ◽

Typed Assembly Language

Download Full-text

Stack-Based Typed Assembly Language

10.21236/ada358572 ◽

1998 ◽

Cited By ~ 28

Author(s):

Greg Morrisett ◽

Karl Crary ◽

David Walker ◽

Neal Glew

Keyword(s):

Assembly Language ◽

Typed Assembly Language

Download Full-text

Stack-based typed assembly language

Journal of Functional Programming ◽

10.1017/s0956796802004446 ◽

2003 ◽

Vol 13 (5) ◽

pp. 957-959 ◽

Cited By ~ 4

Author(s):

GREG MORRISETT ◽

KARL CRARY ◽

NEAL GLEW ◽

DAVID WALKER

Keyword(s):

Assembly Language ◽

Typed Assembly Language

Download Full-text

Construction of a Semantic Model for a Typed Assembly Language

Lecture Notes in Computer Science - Verification, Model Checking, and Abstract Interpretation ◽

10.1007/978-3-540-24622-0_4 ◽

2004 ◽

pp. 30-43 ◽

Cited By ~ 6

Author(s):

Gang Tan ◽

Andrew W. Appel ◽

Kedar N. Swadi ◽

Dinghao Wu

Keyword(s):

Assembly Language ◽

Semantic Model ◽

Typed Assembly Language

Download Full-text

Compilación de programas seguros

10.35537/10915/4205 ◽

2010 ◽

Author(s):

◽

Enrique Molinari

Keyword(s):

Assembly Language ◽

Typed Assembly Language

Este trabajo primero presenta un lenguaje de alto nivel junto con un sistema de tipos que garantiza que los programas bien tipados satisfacen no-interferencia. Luego presenta un lenguaje de bajo nivel basado en Typed Assembly Language, al que denominamos SecTAL (Secure Typed Assembly Language), junto con un sistema de tipos que satisface propiedades similares. Finalmente, presenta una función de compilación junto con una demostración de que preserva la propiedad de no-interferencia. La función de compilación ha sido implementada al igual que un chequeador de tipos para SecTAL1. Las contribuciones pueden resumirse de la siguiente manera: La definición de una función de compilación de un lenguaje imperativo sencillo hacia un lenguaje de bajo nivel basado en Typed Assembly Language. La prueba de un resultado de preservación de tipado que muestra que si el programa fuente es bien tipado (y por ende seguro) también lo será el resultado de compilar el mismo.

Download Full-text