Case
File
Presentation date
Certification approved date
2023-09 FV SHA-256
2023-10-02
2023-11-10
General details
Presented by
Address
Country
Tax id
Represented by
Position
Public Name for public certified software
Formal Vindications S.L
Carrer del Bruc, 21, 2º-4ª, Barcelona
Spain
B66843327
Guillermo Errezil
Main Manager
FV SHA-256
Formally Verified Parts
| File name | Components | Checksum | ||
|---|---|---|---|---|
| SHA256_spec.v | Σ | e098bcec27c8bc4c37a3fcc3b637a9d8713d2b99d751d1d1a4a5794c47db18ba | ||
| correspondence.v | Σ, Δ | 955931d63d60ab28d0a4fe1c8f50b07a4bb0164eb8eafccb902f3defb15ead3e | ||
| N_sha256.v | Π, Δ | 30e477373d3480d11457ea61e20027095c5326016fa003814c0e3afe6e4b5f32 | ||
| extraction.v | Π | 76494f6b97cc6779a064997bb93abd959fb9ad6764b527d6abc7a717c20ef00c | ||
| ssrnat_sha.v | Δ | 219b0fcdeb04185770a606d4613a0ba767b6af449e52c76c0f79b2776ea06e13 | ||
| N_sha.v | Δ | f7a6d1fb96061295660b1208edaa0e2aa85179128c22eba9c41f1bfa37ed9402 | ||
| seq_sha.v | Δ | 85796b0039f0e9148f9ffc355c36e55d56c6c0280deee5060b1c12b8c50a908b | ||
| N_ssrnat_sha.v | Δ | 814c4cb96dae1ff1ea6d2a1f5776ddce598676ab9349b5f31a1f18f912ba9342 | ||
| fi_seq_utils.v | Δ | e01f64ad0a31b8e1fd3eab478b2ed0029c474d4ae1c8c3c3074d3c934e881e87 | ||
| sha256E.ml* | Λ | fc12bbc128e125604abea2d6cbb52506d1414dc406d0d5d2a3ee335db1284f6d | ||
| sha256E.mli* | Λ | 3bd23fd6c0f96a62bfd884947d8db1ebb3bd782e739e90e110fa34cc7e35ed17 | ||
Non Formally Verified Parts
| File name | Components | Checksum | ||
|---|---|---|---|---|
| fv-sha256-phi.pdf | Φ | e73906b23a06c8410568beaa6e446e8156226a74cbbecd34a9db12740917d89e | ||
Other presented parts
| File name | Description | Checksum | ||
|---|---|---|---|---|
| uint63.mli | Interface for OCaml machine integers, provided by Coq | 83d67014936c9a2e6007f2a16e7a40446de7bd505fad7a19b60f98ae6f61f8c1 | ||
| uint63.ml | Code for OCaml machine integers, provided by Coq | 46e6a6412db8dab76aea9b0fab125ea2251f8628f16291f30ed2042f31cd5d16 | ||
| sha.exe | Compiled command-line interface for Windows | 5f328b8c923b9e2314fb2e6f5e857b505112bfca5e626e06721f35bb8ec717cf | ||
| shae.ml | Code for command-line interface, written by FV | 7431ae9de34e1610ccd45376bc1fd5cd7582f1aa6cbbc8ece7c62cd2bda1a227 | ||
| NIST.FIPS.180-4.pdf | A publication describing the standard for secure hash computation using SHA, promulgated under the provisions of FISMA, written by the US Department of Commerce together with the National Institute of Standards and Technology. | 0455b406d89648d20cbde375561e19c245b9815e894164c2670772e3d54deb82 | ||