More Web Proxy on the site http://driver.im/

Article

A typed assembly language for confidentiality

Authors:

Nayeem IslamAuthors Info & Claims

ESOP'06: Proceedings of the 15th European conference on Programming Languages and Systems

Pages 162 - 179

https://doi.org/10.1007/11693024_12

Published: 27 March 2006 Publication History

Abstract

Language-based information-flow analysis is promising in protecting data confidentiality. Although much work has been carried out in this area, relatively little has been done for assembly code. Source-level techniques do not easily generalize Techniques at a source level do not generalize straightforwardly to assembly code, because assembly code does not readily present certain abstraction about the program structure that is crucial to information-flow analysis. Nonetheless, low-level information-flow analysis is desirable, because it yields a small trusted computing base. Furthermore, many (untrusted) applications are distributed in native code; their verification should not be overlooked.

We present a simple yet effective solution for this problem. Our observation is that the missing abstraction in assembly code can be restored using annotations. Following the philosophy of certifying compilation, these annotations are generated by a compiler, used for static validation, and erased before execution. In particular, we propose a type system for low-level information-flow analysis. Our system is compatible with Typed Assembly Language, and models key features including a call stack, memory tuples and first-class code pointers. A noninterference theorem articulates that well-typed programs respect confidentiality. We also present a security-type preserving translation that targets our system, together with its soundness theorem. This illustrates the application of certifying compilation for noninterference.

References

[1]

M. Abadi, A. Banerjee, H. Heintze, and J. G. Riecke. A core calculus of dependency. In Proc. 26th ACM Symp. on Prin. of Prog. Lang., pages 147-160, San Antonio, TX, Jan. 1999.

Digital Library

[2]

J. Agat. Transforming out timing leaks. In Proc. 27th ACM Symposium on Principles of Programming Languages, pages 40-53, Boston, MA, Jan. 2000.

Digital Library

[3]

J. Agat. Type Based Techniques for Covert Channel Elimination and Register Allocation. PhD thesis, Chalmers Univ. of Tech. and Gothenburg Univ., Gothenburg, Sweden, Dec. 2000.

[4]

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

Digital Library

[5]

A. Banerjee and D. A. Naumann. Secure information flow and pointer confinement in a Java-like language. In Proc. 15th IEEE CSFW Workshop, pages 253-267, June 2002.

Digital Library

[6]

G. Barthe, A. Basu, and T. Rezk. Security types preserving compilation. In Proc. 5th International Conf. on VMCAI, volume 2937 of LNCS, pages 2-15, Venice, Italy, Jan. 2004.

[7]

E. Bonelli, A. Compagnoni, and R. Medel. SIFTAL: A typed assembly language for secure information flow analysis. Technical report, Stevens Inst. of Tech., Hoboken, NJ, July 2004.

[8]

N. Heintze and J. G. Riecke. The SLam calculus: Programming with security and integrity. In Proc. 25th ACMSymp. on Prin. of Prog. Lang., pages 365-377, San Diego, CA, Jan. 1998.

Digital Library

[9]

R. Medel, A. Compagnoni, and E. Bonelli. Non-interference for a typed assembly language. In Proc. 2005 Workshop on Foundations of Computer Security, Chicago, IL, June 2005.

Digital Library

[10]

G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-based typed assembly language. Journal of Functional Programming, 12(1):43-88, Jan. 2002.

Digital Library

[11]

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

Digital Library

[12]

A. C. Myers. JFlow: Practical mostly-static information flow control. In Proc. 26th ACM Symp. on Prin. of Prog. Lang., pages 228-241, San Antonio, TX, 1999.

Digital Library

[13]

F. Pottier and V. Simonet. Information flow inference for ML. ACM Transactions on Programming Languages and Systems, 25(1):117-158, Jan. 2003.

Digital Library

[14]

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

Digital Library

[15]

J. H. Saltzer and M. D. Schroeder. The protection of information in computer systems. Proc. of the IEEE, 63(9), Sept. 1975.

[16]

F. B. Schneider, G. Morrisett, and R. Harper. A language-based approach to security. In Informatics: 10 Years Back, 10 Years Ahead, volume 2000 of LNCS, pages 86-101, 2001.

Digital Library

[17]

F. Smith, D. Walker, and G. Morrisett. Alias types. In Proc. 9th European Symposium on Programming, volume 1782 of LNCS, pages 366-381, Berlin, Germany, Apr. 2000.

Digital Library

[18]

G. Smith and D. Volpano. Secure information flow in a multi-threaded imperative language. In Proc. 25th ACMSymp. on Prin. of Prog. Lang., pages 355-364, San Diego, CA, Jan. 1998.

Digital Library

[19]

D. Volpano and G. Smith. Eliminating covert flows with minimum typings. In 10th IEEE Computer Security Foundations Workshop, pages 156-169, Washington, DC, June 1997.

Digital Library

[20]

D. Volpano and G. Smith. A type-based approach to program security. In Proc. 7th Inter. Joint Conf. CAAP/FASE TAPSOFT, LNCS, pages 607-621, Lille, France, Apr. 1997.

Digital Library

[21]

D. Volpano and G. Smith. Probabilistic noninterference in a concurrent language. In Proc. 11th IEEE CSFW Workshop, pages 34-43, Washington, DC, June 1998.

Digital Library

[22]

H. Xi and R. Harper. A dependently typed assembly language. In Proc. 6th ACM International Conference on Functional Programming, pages 169-180, Florence, Italy, Sept. 2001.

Digital Library

[23]

D. Yu and N. Islam. A typed assembly language for confidentiality. Technical Report DCLTR- 2005-0002, DoCoMo Communications Laboratories USA, San Jose, CA, Mar. 2005. http://www.docomolabsresearchers-usa.com/~dyu/talc-tr.pdf.

[24]

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

Digital Library

Cited By

Patrignani MAhmed AClarke D(2019)Formal Approaches to Secure CompilationACM Computing Surveys10.1145/328098451:6(1-36)Online publication date: 4-Feb-2019
https://dl.acm.org/doi/10.1145/3280984
Chen JChugh RSwamy N(2010)Type-preserving compilation of end-to-end verification of security enforcementACM SIGPLAN Notices10.1145/1809028.180664345:6(412-423)Online publication date: 5-Jun-2010
https://dl.acm.org/doi/10.1145/1809028.1806643
Chen JChugh RSwamy NZorn BAiken A(2010)Type-preserving compilation of end-to-end verification of security enforcementProceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1806596.1806643(412-423)Online publication date: 5-Jun-2010
https://dl.acm.org/doi/10.1145/1806596.1806643
Show More Cited By

Recommendations

From system F to typed assembly language

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 ...
Inferable object-oriented typed assembly language
PLDI '10: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation

A certifying compiler preserves type information through compilation to assembly language programs, producing typed assembly language (TAL) programs that can be verified for safety independently so that the compiler does not need to be trusted. There ...
Inferable object-oriented typed assembly language
PLDI '10

A certifying compiler preserves type information through compilation to assembly language programs, producing typed assembly language (TAL) programs that can be verified for safety independently so that the compiler does not need to be trusted. There ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ESOP'06: Proceedings of the 15th European conference on Programming Languages and Systems

March 2006

342 pages

ISBN:354033095X

Editor:
Peter Sestoft
IT University of Copenhagen, Denmark

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 March 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Patrignani MAhmed AClarke D(2019)Formal Approaches to Secure CompilationACM Computing Surveys10.1145/328098451:6(1-36)Online publication date: 4-Feb-2019
https://dl.acm.org/doi/10.1145/3280984
Chen JChugh RSwamy N(2010)Type-preserving compilation of end-to-end verification of security enforcementACM SIGPLAN Notices10.1145/1809028.180664345:6(412-423)Online publication date: 5-Jun-2010
https://dl.acm.org/doi/10.1145/1809028.1806643
Chen JChugh RSwamy NZorn BAiken A(2010)Type-preserving compilation of end-to-end verification of security enforcementProceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1806596.1806643(412-423)Online publication date: 5-Jun-2010
https://dl.acm.org/doi/10.1145/1806596.1806643
Yoshihama SYoshizawa TWatanabe YKudoh MOyanagi K(2007)Dynamic information flow control architecture for web applicationsProceedings of the 12th European conference on Research in Computer Security10.5555/2393847.2393872(267-282)Online publication date: 24-Sep-2007
https://dl.acm.org/doi/10.5555/2393847.2393872
Yu D(2007)More typed assembly languages for confidentialityProceedings of the 5th Asian conference on Programming languages and systems10.5555/1784774.1784784(86-104)Online publication date: 29-Nov-2007
https://dl.acm.org/doi/10.5555/1784774.1784784
Barthe GPichardie DRezk T(2007)A certified lightweight non-interference java bytecode verifierProceedings of the 16th European Symposium on Programming10.5555/1762174.1762189(125-140)Online publication date: 24-Mar-2007
https://dl.acm.org/doi/10.5555/1762174.1762189
Yu D(2007)More Typed Assembly Languages for ConfidentialityProgramming Languages and Systems10.1007/978-3-540-76637-7_7(86-104)Online publication date: 29-Nov-2007
https://dl.acm.org/doi/10.1007/978-3-540-76637-7_7

View Options

View options

Media

Figures

Other

Tables

View Table of Contents