DocumentCode :
3129434
Title :
By reason and authority: a system for authorization of proof-carrying code
Author :
Whitehead, Nathan ; Abadi, Martín ; Necula, George
Author_Institution :
Dept. of Comput. Sci., California Univ., Santa Cruz, CA, USA
fYear :
2004
fDate :
28-30 June 2004
Firstpage :
236
Lastpage :
250
Abstract :
We present a system, BLF, that combines an authorization logic based on the Binder language with a logical framework, LF, able to express semantic properties of programs. BLF is a general system for specifying and enforcing policies that rely on both reason and trust. In particular, BLF supports extensible software systems that employ both digitally signed code and language-based security, especially proof-carrying code. We describe BLF, establish some of its fundamental properties, and explain its use.
Keywords :
digital signatures; formal logic; logic programming; program verification; programming language semantics; theorem proving; BLF; Binder language; authorization logic; digital signature; logical framework; program semantics; proof-carrying code; Authorization; Computer science; Control systems; Data security; Digital signatures; Logic; Open systems; Safety; Software systems; Stability;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Computer Security Foundations Workshop, 2004. Proceedings. 17th IEEE
ISSN :
1063-6900
Print_ISBN :
0-7695-2169-X
Type :
conf
DOI :
10.1109/CSFW.2004.1310744
Filename :
1310744
Link To Document :
بازگشت