scholarly journals Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System

2021 ◽  
Vol 28 (4) ◽  
pp. 372-393
Author(s):  
Dmitry A. Kondratyev
Keyword(s):  
Automatic Parallelization ◽  
Parallel Execution ◽  
Programming System ◽  
Inference Rules ◽  
Deductive Verification ◽  
Recursive Functions ◽  
Axiomatic Semantics ◽  
Verification Conditions ◽  
Symbolic Method ◽  
Verification Condition

The C-lightVer system is developed in IIS SB RAS for C-program deductive verification. C-kernel is an intermediate verification language in this system. Cloud parallel programming system (CPPS) is also developed in IIS SB RAS. Cloud Sisal is an input language of CPPS. The main feature of CPPS is implicit parallel execution based on automatic parallelization of Cloud Sisal loops. Cloud-Sisal-kernel is an intermediate verification language in the CPPS system. Our goal is automatic parallelization of such a superset of C that allows implementing automatic verification. Our solution is such a superset of C-kernel as C-Sisal-kernel. The first result presented in this paper is an extension of C-kernel by Cloud-Sisal-kernel loops. We have obtained the C-Sisal-kernel language. The second result is an extension of C-kernel axiomatic semantics by inference rule for Cloud-Sisal-kernel loops. The paper also presents our approach to the problem of deductive verification automation in the case of finite iterations over data structures. This kind of loops is referred to as definite iterations. Our solution is a composition of symbolic method of verification of definite iterations, verification condition metageneration and mixed axiomatic semantics method. Symbolic method of verification of definite iterations allows defining inference rules for these loops without invariants. Symbolic replacement of definite iterations by recursive functions is the base of this method. Obtained verification conditions with applications of recursive functions correspond to logical base of ACL2 prover. We use ACL2 system based on computable recursive functions. Verification condition metageneration allows simplifying implementation of new inference rules in a verification system. The use of mixed axiomatic semantics results to simpler verification conditions in some cases.

Towards verification of scientific and engineering programs. The CPPS project

2020 ◽  
pp. 91-106
Author(s):  
Дмитрий Алексеевич Кондратьев ◽  
Алексей Владимирович Промский
Keyword(s):  
Parallel Programming ◽  
Program Verification ◽  
Array Element ◽  
Programming System ◽  
Deductive Verification ◽  
Engineering Applications ◽  
Engineering Programs ◽  
Domain Specific ◽  
Axiomatic Semantics ◽  
Engineering Mathematics

В настоящее время, когда теоретические основы верификации программ хорошо изучены, исследователи концентрируют свои усилия на предметно-ориентированных методах для различных классов программ. Инструменты, которые они выбирают, варьируются от проверки моделей для сетевых протоколов до исчислений указателей для фрагментов ядра операционной системы. Однако, похоже, что области научных и инженерных программ все еще уделяется недостаточно внимания. Мы хотели бы внести свой вклад в заполнение этого пробела с помощью разработки системы CPPS. Целью этого проекта является создание системы параллельного программирования для Sisal-программ. Дедуктивная верификация Sisal-программ является одной из важных подцелей. Так как язык Cloud-Sisal построен на основе циклических выражений, их аксиоматическая семантика является базой логики Хоара для языка Sisal. Циклические выражения языка Cloud-Sisal, выражения конструирования массивов и выражения замещения элементов массивов позволяют реализовать эффективно исполняемые программы вычислительной или инженерной математики. Таким образом, мы полагаем, что наша аксиоматическая семантика для этих типов выражений может представлять интересный результат. Природа таких программ позволяет достичь не только эффективного исполнения, но и упростить верификацию. Действительно, программы вычислительной математики часто основаны на итерациях над структурами данных. Символический метод верификации финитных итераций является в этой ситуации очень полезным, так как он элиминирует те проблемные инварианты цикла, которые всегда мешают формальной верификации. Все предыдущие исследования этого метода были теоретическими, CPPS представляет собой первую попытку использования его на практике. Nowadays, when formal fundamentals of program verification are well studied, researchers concentrate their efforts on domain-specific methods for various classes of programs. However, it seems that the field of scientific and engineering applications still lacks attention. We would like to contribute to filling this gap through the development of the Cloud Parallel Programming System (CPPS). The goal of this project is to create a parallel programming system for Sisal programs. Deductive verification of Sisal programs is one the of important subgoals. Since the Cloud Sisal language is built on the basis of loop expressions, their axiomatic semantics is the basis of Hoare’s logic for the Sisal language. The Cloud Sisal loop expressions, array construction expressions and array element replacement expressions enable efficiently executable computational or engineering mathematics programs. Thus, we believe that our axiomatic semantics for these types of expressions may present an interesting result.

scholarly journals The Automation of C Program Verification by Symbolic Method of Loop Invariants Elimination

2018 ◽  
Vol 25 (5) ◽  
pp. 491-505
Author(s):  
Dmitry Kondratyev ◽  
Ilya Maryasov ◽  
Valery Nepomniaschy
Keyword(s):  
Program Verification ◽  
Inference Rule ◽  
Automated System ◽  
Symbolic Form ◽  
Verification Method ◽  
Axiomatic Semantics ◽  
Verification Conditions ◽  
Loop Body ◽  
Symbolic Method ◽  
Replacement Operation

During deductive verification of programs written in imperative languages, the generation and proof of verification conditions corresponding to loops can cause difficulties, because each one must be provided with an invariant whose construction is often a challenge. As a rule, the methods of invariant synthesis are heuristic ones. This impedes its application. An alternative is the symbolic method of loop invariant elimination suggested by V.A. Nepomniaschy in 2005. Its idea is to represent a loop body in a form of special replacement operation under certain constraints. This operation expresses loop effect in a symbolic form and allows to introduce an inference rule which uses no invariants in axiomatic semantics. This work represents the further development of this method. It extends the mixed axiomatic semantics method suggested for C-light program verification. This extension includes the verification method of iterations over changeable arrays possibly with loop exit in C-light programs. The method contains the inference rule for iterations without loop invariants. This rule was implemented in verification conditions generator which is a part of the automated system of C-light program verification. To prove verification conditions automatically in ACL2, two algorithms were developed and implemented. The first one automatically generates the replacement operation in ACL2 language, the second one automatically generates auxiliary lemmas which allow to prove the obtained verification conditions in ACL2 successfully in automatic mode. An example which illustrates the application of the mentioned methods is described.

Algorithmic Logic with Recursive Functions

1981 ◽  
Vol 4 (4) ◽  
pp. 975-995
Author(s):  
Andrzej Szałas
Keyword(s):  
Completeness Theorem ◽  
Inference Rules ◽  
Partial Correctness ◽  
Recursive Functions ◽  
Algorithmic Logic ◽  
Block Structured

A language is considered in which the reader can express such properties of block-structured programs with recursive functions as correctness and partial correctness. The semantics of this language is fully described by a set of schemes of axioms and inference rules. The completeness theorem and the soundness theorem for this axiomatization are proved.

scholarly journals Investigation of Data Dependencies by Dynamic Analysis of Sapfor

2020 ◽  
Vol 23 (3) ◽  
pp. 473-493
Author(s):  
Nikita Andreevich Kataev ◽  
Alexander Andreevich Smirnov ◽  
Andrey Dmitrievich Zhukov
Keyword(s):  
Dynamic Analysis ◽  
Programming Languages ◽  
Static Analysis ◽  
Automatic Parallelization ◽  
Parallel Execution ◽  
Control Flow ◽  
Analysis Tool ◽  
Data Dependencies ◽  
Program Parallelization ◽  
Memory Accesses

The use of pointers and indirect memory accesses in the program, as well as the complex control flow are some of the main weaknesses of the static analysis of programs. The program properties investigated by this analysis are too conservative to accurately describe program behavior and hence they prevent parallel execution of the program. The application of dynamic analysis allows us to expand the capabilities of semi-automatic parallelization. In the SAPFOR system (System FOR Automated Parallelization), a dynamic analysis tool has been implemented, based on on the instrumentation of the LLVM representation of an analyzed program, which allows the system to explore programs in both C and Fortran programming languages. The capabilities of the static analysis implemented in SAPFOR are used to reduce the overhead program execution, while maintaining the completeness of the analysis. The use of static analysis allows to reduce the number of analyzed memory accesses and to ignore scalar variables, which can be explored in a static way. The developed tool was tested on performance tests from the NAS Parallel Benchmarks package for C and Fortran languages. The implementation of dynamic analysis, in addition to traditional types of data dependencies (flow, anit, output), allows us to determine privitizable variables and a possibility of pipeline execution of loops. Together with the capabilities of DVM and OpenMP these greatly facilitates program parallelization and simplify insertion of the appropriate compiler directives.

scholarly journals Solving constrained Horn clauses modulo algebraic data types and recursive functions

2022 ◽  
Vol 6 (POPL) ◽  
pp. 1-29
Author(s):  
Hari Govind V K ◽  
Sharon Shoham ◽  
Arie Gurfinkel
Keyword(s):  
Data Structures ◽  
General Class ◽  
Data Types ◽  
Deductive Verification ◽  
Recursive Definition ◽  
Underlying Theory ◽  
Horn Clauses ◽  
Verification Conditions ◽  
Algebraic Data Types ◽  
Inductive Invariants

This work addresses the problem of verifying imperative programs that manipulate data structures, e.g., Rust programs. Data structures are usually modeled by Algebraic Data Types (ADTs) in verification conditions. Inductive invariants of such programs often require recursively defined functions (RDFs) to represent abstractions of data structures. From the logic perspective, this reduces to solving Constrained Horn Clauses (CHCs) modulo both ADT and RDF. The underlying logic with RDFs is undecidable. Thus, even verifying a candidate inductive invariant is undecidable. Similarly, IC3-based algorithms for solving CHCs lose their progress guarantee: they may not find counterexamples when the program is unsafe. We propose a novel IC3-inspired algorithm Racer for solving CHCs modulo ADT and RDF (i.e., automatically synthesizing inductive invariants, as opposed to only verifying them as is done in deductive verification). Racer ensures progress despite the undecidability of the underlying theory, and is guaranteed to terminate with a counterexample for unsafe programs. It works with a general class of RDFs over ADTs called catamorphisms. The key idea is to represent catamorphisms as both CHCs, via relationification , and RDFs, using novel abstractions . Encoding catamorphisms as CHCs allows learning inductive properties of catamorphisms, as well as preserving unsatisfiabilty of the original CHCs despite the use of RDF abstractions, whereas encoding catamorphisms as RDFs allows unfolding the recursive definition, and relying on it in solutions. Abstractions ensure that the underlying theory remains decidable. We implement our approach in Z3 and show that it works well in practice.

Axiomatic semantics of projection temporal logic programs

2010 ◽  
Vol 20 (5) ◽  
pp. 865-914 ◽  
Author(s):  
XIAOXIAO YANG ◽  
ZHENHUA DUAN ◽  
QIAN MA
Keyword(s):  
Temporal Logic ◽  
Axiom System ◽  
Automatic Verification ◽  
Inference Rules ◽  
Hoare Logic ◽  
Logic Programs ◽  
Operational Model ◽  
Current State ◽  
Axiomatic Semantics ◽  
State Inference

In this paper, we investigate the axiomatic semantics of the projection temporal logic programming language MSVL. To this end, we employ Propositional Projection Temporal Logic (PPTL) as an assertion language to specify the desired properties. We give a set of state axioms and state inference rules. In order to deduce a program over an interval, we also formalise a set of rules in terms of a Hoare logic-like triple. These rules enable us to deduce a program into its normal form and from the current state to the next one. They also enable us to verify properties over intervals. In this way, an axiom system for proving the correctness of MSVL programs is established. The axiom system is proved to be sound and relatively complete with respect to an operational model of MSVL, and give an example showing how the axiom system works. Finally, we employ a recently developed prototype verifier based on PVS as an example of semi-automatic verification using MSVL.

scholarly journals Symbolic Approach for Side-Channel Resistance Analysis of Masked Assembly Codes

10.29007/hhnf ◽  
2018 ◽  
Author(s):  
Inès Ben El Ouahma ◽  
Quentin Meunier ◽  
Karine Heydemann ◽  
Emmanuelle Encrenaz
Keyword(s):  
Source Code ◽  
Side Channel ◽  
Inference Rules ◽  
Side Channel Attacks ◽  
Secret Data ◽  
Source Codes ◽  
Resistance Analysis ◽  
Channel Resistance ◽  
Symbolic Method ◽  
Symbolic Approach

Masking is a popular countermeasure against side-channel attacks, that randomizes secret data with random and uniform variables called masks. At software level, masking is usually added in the source code and its effectiveness needs to be verified. In this paper, we propose a symbolic method to verify side-channel robustness of masked programs. The analysis is performed at the assembly level since compilation and optimizations may alter the added protections. Our proposed method aims to verify that intermediate computations are statistically independent from secret variables using defined distribution inference rules. We verify the first round of a masked AES in 22s and show that some secure algorithms or source codes are not leakage-free in their assembly implementations.

Sign in / Sign up

Export Citation Format

Share Document