A 2005

CRC64 Algorithm Analysis and Verification

ŠAFRÁNEK, David; Vojtěch ŘEHÁK; Tomáš KRATOCHVÍLA; Pavel ŠIMEČEK; Petr HLÁVKA et. al.

Základní údaje

Originální název

CRC64 Algorithm Analysis and Verification

Název česky

CRC64 Algorithm Analysis and Verification

Autoři

ŠAFRÁNEK, David (203 Česká republika, garant); Vojtěch ŘEHÁK (203 Česká republika); Tomáš KRATOCHVÍLA (203 Česká republika); Pavel ŠIMEČEK (203 Česká republika); Petr HLÁVKA (203 Česká republika) a Tomáš VOJNAR (203 Česká republika)

Vydání

Brno, Technical Report 27/2005, 2005

Nakladatel

CESNET, z. s. p. o.

Další údaje

Jazyk

angličtina

Typ výsledku

Audiovizuální tvorba

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

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

Odkazy

Kód RIV

RIV/00216224:14330/05:00012922

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

CRC64; formal verification; correctness of CRC algorithm

Štítky

Změněno: 2. 5. 2008 13:57, RNDr. Pavel Šimeček, Ph.D.

Anotace

ORIG CZ

V originále

This work analyzes the use of a CRC64 algorithm as a hashing function in the Netflow project. We describe the basis of Cyclic Redundancy Check (CRC) algorithms and consider properties like collision probability, Hamming distance, and quality of distribution, which are crucial for hashing functions. Lower or upper bounds of these properties are described mathematically. However, to give more precise numbers to hardware designers, we also try to find them using model checking method.

Česky

Zpráva obsahuje analýzu a verifikaci algoritmu implementovaného v hardware pro kontrolní součet CRC64. Základy algoritmu CRC jsou popsány v první části právce, po té jsou stanoveny klíčové vlastnosti zaručující korektnost - pravděpodobnost kolize, Hammingova vzálenost a kvalita distribuce hašujících funkcí.

Návaznosti

GA201/03/0509, projekt VaV
Název: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
GD102/05/H050, projekt VaV
Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
MSM0021622419, záměr
Název: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET408050503, projekt VaV
Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů