scholarly journals Hardware-Assisted Program Execution Integrity: HAPEI

2018 ◽  
pp. 405-420
Author(s):  
Ronan Lashermes ◽  
Hélène Le Bouder ◽  
Gaël Thomas
Keyword(s):  
Program Execution

Tracking P4 Program Execution in the Data Plane

2020 ◽  
Author(s):  
Suriya Kodeswaran ◽  
Mina Tahmasbi Arashloo ◽  
Praveen Tammana ◽  
Jennifer Rexford
Keyword(s):  
Program Execution ◽  
Data Plane

A Logically Justified Model of Computation I

1981 ◽  
Vol 4 (1) ◽  
pp. 151-172
Author(s):  
Pierangelo Miglioli ◽  
Mario Ornaghi
Keyword(s):  
Computer Science ◽  
Program Synthesis ◽  
Completeness Theorem ◽  
Point Of View ◽  
Program Execution ◽  
Computation Model ◽  
Clear Explanation ◽  
Direct Interpretation ◽  
Adequacy Condition ◽  
General Explanation

The aim of this paper is to provide a general explanation of the “algorithmic content” of proofs, according to a point of view adequate to computer science. Differently from the more usual attitude of program synthesis, where the “algorithmic content” is captured by translating proofs into standard algorithmic languages, here we propose a “direct” interpretation of “proofs as programs”. To do this, a clear explanation is needed of what is to be meant by “proof-execution”, a concept which must generalize the usual “program-execution”. In the first part of the paper we discuss the general conditions to be satisfied by the executions of proofs and consider, as a first example of proof-execution, Prawitz’s normalization. According to our analysis, simple normalization is not fully adequate to the goals of the theory of programs: so, in the second section we present an execution-procedure based on ideas more oriented to computer science than Prawitz’s. We provide a soundness theorem which states that our executions satisfy an appropriate adequacy condition, and discuss the sense according to which our “proof-algorithms” inherently involve parallelism and non determinism. The Properties of our computation model are analyzed and also a completeness theorem involving a notion of “uniform evaluation” of open formulas is stated. Finally, an “algorithmic completeness” theorem is given, which essentially states that every flow-chart program proved to be totally correct can be simulated by an appropriate “purely logical proof”.

Exploiting non-uniform program execution time to evade record/replay forensic analysis

2020 ◽  
Vol 88 ◽  
pp. 101516
Author(s):  
Yang Hu ◽  
Mingshen Sun ◽  
John C.S. Lui
Keyword(s):  
Execution Time ◽  
Forensic Analysis ◽  
Program Execution

AUTOMATIC RESULT VERIFICATION BY COMPLETE RUN-TIME CHECKING OF COMPUTATIONS

2001 ◽  
Vol 12 (01) ◽  
pp. 97-124 ◽  
Author(s):  
EDGAR F. A. LEDERER ◽  
ROMEO A. DUMITRESCU
Keyword(s):  
Programming Language ◽  
Error Detection ◽  
Program Execution ◽  
Good Efficiency ◽  
Result Verification ◽  
Coordination Model ◽  
Functional Specification ◽  
Time Result ◽  
Run Time

Two-Stage Programming (2SP) is an experimental programming language, the first implementation of the Specification-Consistent Coordination Model (SCCM). The SCCM proposes a new, mixed-paradigm (functional/imperative) approach to developing reliable programs based on complete run-time checking of computations with respect to a given specification. A 2SP program consists of a functional specification and an imperative coordination tightly connected to the specification. The coordination maps the specification to an imperative and possibly parallel/distributed program. Normal termination of a 2SP program execution implies the correctness of the computed results with respect to the specification, for that execution. We present the basic feautures of the SCCM/2SP, a new message-spassing system of 2SP with integrated run-time checking, and a larger case study. We show that 2SP provides: functional specifications, specification-consistent imperative coordinations, automatic run-time result verification and error detection, enhanced debugging support, and good efficiency.

Sign in / Sign up

Export Citation Format

Share Document