Encoding the program correctness proofs as programs in PCC technology

被引：0
|
作者：
Pirzadeh, Heidar [1 ]
Dube, Danny [2 ]
机构：
[1] Univ Montreal, DIRO, CP 6128 Succ Ctr Ville, Montreal, PQ H3C 3J7, Canada
[2] Univ Laval, Dept Dinformatique genie logical, Quebec City, PQ G1K 7P4, Canada
来源：
SIXTH ANNUAL CONFERENCE ON PRIVACY, SECURITY AND TRUST, PROCEEDINGS | 2008年
基金：
加拿大自然科学与工程研究理事会;
关键词：
D O I：
10.1109/PST.2008.20
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
One of the key issues with the practical applicability of Proof-Carrying Code (PCC) and its related methods is the difficulty in communi. eating and storing the proofs which are inherently large. The approaches proposed to alleviate this, suffer from drawbacks of their own especially the enlargement of the Trusted Computing Base, in which any bug may cause an unsafe program to be accepted. We propose a generic extended PCC framework (EPCC) in which, instead of the proof a proof generator for the program in question is transmitted. This framework enables the execution of the proof generator and the recovery of the proof on the consumer side in a secure manner
引用
收藏
页码：121 / +
页数：2
相关论文
共 50 条
  • [21] Programming language elements for correctness proofs
    Department of Programming Languages and Compilers, Faculty of Informatics, Eötvös Loránd University, Budapest, Hungary
    Acta Cybern, 2008, 3 (403-425):
  • [22] Functional correctness proofs of encryption algorithms
    Duan, JJ
    Hurd, J
    Li, GD
    Owens, S
    Slind, K
    Zhang, JX
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3835 : 519 - 533
  • [23] Correctness proofs for SCADA communication protocols
    Graham, James H.
    Patel, Sandip C.
    WMSCI 2005: 9th World Multi-Conference on Systemics, Cybernetics and Informatics, Vol 2, 2005, : 392 - 397
  • [24] ABSTRACT IMPLEMENTATIONS AND THEIR CORRECTNESS PROOFS.
    Nourani, C.Farshid
    Journal of the ACM, 1983, 30 (02): : 343 - 359
  • [25] Modular correctness proofs of behavioural implementations
    Michel Bidoit
    Rolf Hennicker
    Acta Informatica, 1998, 35 : 951 - 1005
  • [26] Modular correctness proofs of behavioural implementations
    Bidoit, M
    Hennicker, R
    ACTA INFORMATICA, 1998, 35 (11) : 951 - 1005
  • [27] Programming Language Elements for Correctness Proofs
    Devai, Gergely
    ACTA CYBERNETICA, 2008, 18 (03): : 403 - 425
  • [28] AN ABSTRACT PROGRAMMING LANGUAGE AND CORRECTNESS PROOFS
    LIU, SY
    COMPUTER LANGUAGES, 1993, 18 (04): : 273 - 282
  • [29] Towards practical proofs of class correctness
    Meyer, B
    ZB 2003: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, 2003, 2651 : 359 - 387
  • [30] CORRECTNESS PROOFS OF DISTRIBUTED TERMINATION ALGORITHMS
    APT, KR
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (03): : 388 - 405
12345