Execution Time Program Verication With Tight Bounds Ana Carolina Silva1 Manuel Barbosa12 and M ario Florido13

2025-05-06 0 0 906.1KB 58 页 10玖币

侵权投诉

Execution Time Program Veriﬁcation With

Tight Bounds

Ana Carolina Silva1, Manuel Barbosa1,2, and M´ario Florido1,3

1FCUP, Universidade do Porto

2INESC TEC

3LIACC, Universidade do Porto

Abstract. This paper presents a proof system for reasoning about exe-

cution time bounds for a core imperative programming language. Proof

systems are deﬁned for three diﬀerent scenarios: approximations of the

worst-case execution time, exact time reasoning, and less pessimistic exe-

cution time estimation using amortized analysis. We deﬁne a Hoare logic

for the three cases and prove its soundness with respect to an anno-

tated cost-aware operational semantics. Finally, we deﬁne a veriﬁcation

conditions (VC) generator that generates the goals needed to prove pro-

gram correctness, cost, and termination. Those goals are then sent to the

Easycrypt toolset for validation. The practicality of the proof system is

demonstrated with an implementation in OCaml of the diﬀerent modules

needed to apply it to example programs. Our case studies are motivated

by real-time and cryptographic software.

Keywords: Program Veriﬁcation ·Execution time analysis ·Amortized

analysis ·Hoare logic

1 Introduction

Semantics-based approaches to program veriﬁcation usually belong to two diﬀer-

ent broad classes: 1) partial correctness assertions expressing relations between

the initial and ﬁnal state of program variables in the form of pre and postcondi-

tions, assuming that the program terminates; and 2) total correctness properties,

which besides those assertions which specify claims about program behavior, also

express program termination.

However, another class of properties is fast growing in relevance as a target for

program veriﬁcation: resource consumption when executing a program. The term

resource is used broadly: resources can be time used to execute the program on a

particular architecture, memory used (stack or heap) during program execution,

or even energy consumption. Resource consumption has a signiﬁcant impact in

diﬀerent speciﬁc areas, such as real-time systems, critical systems relying on

limited power sources, and the analysis of timing side-channels in cryptographic

software.

A proof system for total correctness can be used to prove that a program

execution terminates, but it does not give any information about the resources

arXiv:2210.11105v1 [cs.PL] 20 Oct 2022

it needs to terminate. In this dissertation, we want to study extended proof

systems for proving assertions about program behavior that may refer to the

required resources and, in particular, to the execution time.

Proof systems to prove bounds on the execution time of program execution

were deﬁned before in [22,5]. Inspired by the work presented in [5] our goal is

to study inference systems that allow proving assertions of the form {ϕ}C{ψ|t},

meaning that if the execution of the statement Cis started in a state that vali-

dates the precondition ϕthen it terminates in a state that validates postcondition

ψand the required execution time is at most of magnitude t.

2 Goals and Contributions

Our main goal is to deﬁne an axiomatic semantics-based proof system for reason-

ing about execution time bounds for a core imperative programming language.

Such a system would be useful not only to understand the resource necessities

of a program but also it could be applied to cryptographic implementations to

prove the independence of resource usage from certain program variables. This

high-level goal translates into the following concrete objectives:

1. Study axiomatic systems. This will further our knowledge in the ﬁeld and

allow us to understand how to deﬁne our logic for resource analysis.

2. Study amortized analysis so we can understand how to apply amortization

to a proof system to reﬁne cost-bound estimation of while loops.

3. Analyze the state-of-the-art to understand what has already been developed

to analyze resource consumption and the main limitations found.

4. Develop a sound logic capable of verifying correction, terminations, and

bounds on resource consumption using a simple imperative programming

language.

5. Create a tool based on our logic, capable of verifying time bounds, correction,

and terminations, for example-problems.

6. Apply this logic to analyze the time complexity of classic algorithms.

The main contribution of this paper is a proof system that can verify resource

assumptions in three diﬀerent scenarios:

1. Upper bounds on the required execution time. This is mostly an adaptation

of previous work in [5].

2. Amortized costs denoting less pessimistic bounds on the execution time.

3. Exact costs for a fragment of the initial language with bounded recursion

and a constrained form of conditional statements.

The two last scenarios are a novel contribution of our system, and we treat

them in a uniﬁed way to enable their integrated use.

Assertions on program behavior that establish upper bounds on execution

time may be useful for general programming, where one wants to prove safety

conditions concerning the worse case program complexity. As in prior approaches,

the tightness of the bound is not captured by the logic, and there is often a trade-

oﬀ between the tightness of the proved bound and the required proof eﬀort.

Proofs that leverage amortized costs may be used when trivially composing

worst-case run-time bounds results in overly pessimistic analyses. This is partic-

ularly useful for algorithms where some components imply a signiﬁcant cost in

resources, whereas other components are not as costly. With amortized costs, we

may prove assertions about the aggregate use of costly and less costly operations

over the whole algorithm execution.

Finally, the third class of assertions denoting exact costs are useful in sce-

narios where the approximation of execution time is not enough to guarantee

safety, as it happens for critical systems and real-time programming. Moreover,

proving that the exact execution time of a program is an expression that does

not depend on conﬁdential data provides a direct way to prove the absence of

timing leakage, which is relevant in cryptographic implementations. We must

restrict the programming language to guarantee the ability to prove exact costs.

Thus, in this third scenario, programs have bound recursion, and conditional

statement branches have to have the same cost.

Before deﬁning our proof system, we deﬁned an operational semantics capable

of computing the execution time for expressions and statements during program

execution. This cost-aware operational semantics is another contribution of our

work, and it is used to prove the soundness of our inference system.

A third contribution of this work, which shows the practicality of our proof

system, is an implementation in OCaml of the diﬀerent modules needed to apply

it to example programs. We then present several application examples motivated

by real-time and cryptographic software.

3 Document Structure

This document is organized as follows:

–The ﬁrst chapter - Introduction - gives a context of our work in the ﬁeld,

the motivation for this project, our main goals, our contributions, and how

the document is organized.

–The second chapter - Background - elaborates on the theoretical results

used in the basis of our work and needed to understand our deﬁnitions and

results.

–The third chapter - Related Work - presents an analysis of the literature

on static resource analysis, from type-based systems to axiomatic semantics

systems.

–The fourth chapter - Cost Aware Program Logic - presents our language

deﬁnition, our original logic for upper bound estimation, the respective VCG,

and some illustrative examples.

–The ﬁfth chapter - Amortized Costs - brieﬂy introduces the ﬁeld of amor-

tized analysis and presents an extension to the logic and VCG from chapter

4, with the use of amortized analysis to improve the upper-bound estimation.

–The sixth chapter - Exact Logic - presents a variation to our language and

an extension to our logic that allows for the derivation of the exact cost of

a program.

–The seventh chapter - Implementation and Experimental Results -

shows the architecture of the tool developed, as well as some implementation

details and practical results.

–The eighth chapter - Conclusion and Future Work - reﬂects on the main

conclusions from our research and developed work and presents some goals

to further extend and improve our project.

4 Background

In this chapter, we provide an overview of the ﬁeld of formal veriﬁcation and some

of the most relevant theoretical results that are the basis of our work. We start

by giving historical background on the ﬁeld of formal veriﬁcation. Here we will

present results, such as the ones achieved by Floyd and Hoare, used as the base

of our deﬁnitions. We will also deﬁne concepts fundamental to understanding

the work presented in this dissertation.

5 Historical Background

As computers became more powerful, programs also became longer and more

complex. When programs were still relatively small, ﬂowcharts or extensive test-

ing was enough to prove a program’s functionality. But programs quickly started

being so complex that these methods became unreliable and more prone to error.

At the beginning of the second half of the 20th-century, experts started to

ﬁnd vulnerabilities in public distributed software. Since then, the use of computa-

tional systems has grown exponentially, and so did the number of vulnerabilities

and their impact. A simple error might have drastic consequences, such as a

leak of conﬁdential information, the crash of critical systems, and direct loss of

assets.

This problem proved to be enough reason to start thinking about a more

reliable way to guarantee the properties of a program and develop tools that

help verify these properties.

Formal Veriﬁcation refers to using mathematical principles to prove the cor-

rection of a given speciﬁcation of a program. It is hard to pinpoint where it all

started, but the works of Robert Floyd [11] and Tony Hoare [14] were undoubt-

edly pioneers in the ﬁeld, and their deﬁnitions are still the base of veriﬁcation

tools used today.

6 Semantics

When deﬁning programming languages, we want a way to be capable of reason-

ing about what programs are doing. The syntax describes the grammatical rules

we must follow to write a program in a language. The syntax allows us to dis-

tinguish between languages and identify a program’s language. But if we want

to understand what that program is doing, we need to look at its semantics.

Semantics is a way to make sense of the meaning of a program and understand

what it is trying to accomplish.

There are multiple strategies to analyze the meaning of a program. The most

popular ones are operational, denotational, and axiomatic semantics. Opera-

tional semantics focus on what steps we take during the program’s execution. In

denotational semantics, we do not care about the ”how” but only about ”what”

the program is doing. In axiomatic semantics, we are concerned about evaluating

the satisfability of assertions on the program and its variables. We will go more

in-depth on how operational and axiomatic semantics work.

6.1 Operational Semantics

Operational semantics describes the meaning of a program by specifying the

transitions between states of an abstract state machine. As we mentioned, unlike

with denotational semantics, here we are concerned about how the machine

changes states with the execution of a statement.

There are two styles of operational semantics

–Small-step or Structural Operational Semantics

–Big-step or Natural Semantics

In Structural Operational Semantics or Small-step Semantics, we are con-

cerned about every individual transition we take throughout the program’s exe-

cution. In Natural Semantics or Big-step semantics, we want to understand how

we transition from the initial to the ﬁnal state. We are concerned about a high-

level analysis of how the machine state changes and not about each individual

step.

6.2 Axiomatic Semantics (Hoare Logic)

In 1967 Floyd speciﬁed a method that would allow proving properties on pro-

grams, such as correctness, equivalence, and termination [11]. They achieved this

by representing programs as ﬂowcharts and associating propositions to each con-

nection on the ﬂowchart. The proof is done by induction on the number of steps.

If an instruction is reached by a connection whose proposition is true, then we

must leave it with a true condition as well. In 1969 Hoare wrote a paper where

they extended Floyd’s logic to prove properties on a simple imperative program

[14]. In this paper, they deﬁned what we now call Hoare (or Floyd-Hoare) triples.

Deﬁnition 1 (Hoare Triples). A Hoare triple is represented as

{P}Q{R}

and can be interpreted as ”if the assertion Pis true before we run program Q,

then assertion Rwill be true when the program ends”.

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

ExecutionTimeProgramVericationWithTightBoundsAnaCarolinaSilva1,ManuelBarbosa1;2,andMarioFlorido1;31FCUP,UniversidadedoPorto2INESCTEC3LIACC,UniversidadedoPortoAbstract.Thispaperpresentsaproofsystemforreasoningaboutexe-cutiontimeboundsforacoreimperativeprogramminglanguage.Proofsystemsaredenedforthr...

展开>> 收起<<

Execution Time Program Verication With Tight Bounds Ana Carolina Silva1 Manuel Barbosa12 and M ario Florido13.pdf

共58页,预览5页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Execution Time Program Verication With Tight Bounds Ana Carolina Silva1 Manuel Barbosa12 and M ario Florido13

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: