Compiling C and C++ Programs for Dynamic White-Box Analysis

D 2020

Compiling C and C++ Programs for Dynamic White-Box Analysis

BARANOVÁ, Zuzana a Petr ROČKAI

Základní údaje

Originální název

Compiling C and C++ Programs for Dynamic White-Box Analysis

Autoři

BARANOVÁ, Zuzana (703 Slovensko, domácí) a Petr ROČKAI (703 Slovensko, domácí)

Vydání

Cham, Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019), od s. 30-45, 16 s. 2020

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/20:00115150

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-54993-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-54994-7_4

Klíčová slova anglicky

DIVINE; automated compilation; formal verification; model checking; C; C++

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 31. 10. 2020 02:42, RNDr. Petr Ročkai, Ph.D.

Anotace

V originále

Building software packages from source is a complex and highly technical process. For this reason, most software comes with build instructions which have both a human-readable and an executable component. The latter in turn requires substantial infrastructure, which helps software authors deal with two major sources of complexity: first, generation and management of various build artefacts and their dependencies, and second, the differences between platforms, compiler toolchains and build environments. This poses a significant problem for white-box analysis tools, which often require that the source code of the program under test is compiled into an intermediate format, like the LLVM IR. In this paper, we present divcc, a drop-in replacement for C and C++ compilation tools which transparently fits into existing build tools and software deployment solutions. Additionally, divcc generates intermediate and native code in a single pass, ensuring that the final executable is built from the intermediate code that is being analysed.

Citovat

BARANOVÁ, Zuzana a Petr ROČKAI. Compiling C and C++ Programs for Dynamic White-Box Analysis. In Nelma Moreira and Emil Sekerinski. Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019). Cham: Springer International Publishing, 2020, s. 30-45. ISBN 978-3-030-54993-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-54994-7_4.

@inproceedings{1592136,
   author = {Baranová, Zuzana and Ročkai, Petr},
   address = {Cham},
   booktitle = {Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019)},
   doi = {http://dx.doi.org/10.1007/978-3-030-54994-7_4},
   editor = {Nelma Moreira and Emil Sekerinski},
   keywords = {DIVINE; automated compilation; formal verification; model checking; C; C++},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-030-54993-0},
   note = {held as part of the Third World Congress on Formal Methods, FM 2019; to appear},
   pages = {30-45},
   publisher = {Springer International Publishing},
   title = {Compiling C and C++ Programs for Dynamic White-Box Analysis},
   year = {2020}
}

TY  - JOUR
ID  - 1592136
AU  - Baranová, Zuzana - Ročkai, Petr
PY  - 2020
TI  - Compiling C and C++ Programs for Dynamic White-Box Analysis
PB  - Springer International Publishing
CY  - Cham
SN  - 9783030549930
N1  - held as part of the Third World Congress on Formal Methods, FM 2019; to appear
KW  - DIVINE
KW  - automated compilation
KW  - formal verification
KW  - model checking
KW  - C
KW  - C++
N2  - Building software packages from source is a complex and highly technical process. For this reason, most software comes with build instructions which have both a human-readable and an executable component. The latter in turn requires substantial infrastructure, which helps software authors deal with two major sources of complexity: first, generation and management of various build artefacts and their dependencies, and second, the differences between platforms, compiler toolchains and build environments. This poses a significant problem for white-box analysis tools, which often require that the source code of the program under test is compiled into an intermediate format, like the LLVM IR. In this paper, we present divcc, a drop-in replacement for C and C++ compilation tools which transparently fits into existing build tools and software deployment solutions. Additionally, divcc generates intermediate and native code in a single pass, ensuring that the final executable is built from the intermediate code that is being analysed.
ER  -

BARANOVÁ, Zuzana a Petr ROČKAI. Compiling C and C++ Programs for Dynamic White-Box Analysis. In Nelma Moreira and Emil Sekerinski. \textit{Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019)}. Cham: Springer International Publishing, 2020, s.~30-45. ISBN~978-3-030-54993-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-54994-7\_{}4.

Podrobný výpis o publikaci