Commit 4b63da9f authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[x509-parser] updated wrt to ANSSI Github

parent 15f61729
Pipeline #35869 passed with stage
in 55 minutes and 44 seconds
......@@ -7,7 +7,7 @@ Coverage estimation = 100.0%
------------------------------------
[metrics] Statements analyzed by Eva
--------------------------
3107 stmts in analyzed functions, 2955 stmts analyzed (95.1%)
3112 stmts in analyzed functions, 2960 stmts analyzed (95.1%)
_extract_complex_tag: 39 stmts out of 39 (100.0%)
_is_alpha: 11 stmts out of 11 (100.0%)
_is_digit: 6 stmts out of 6 (100.0%)
......@@ -32,7 +32,7 @@ parse_rdn_val_state: 2 stmts out of 2 (100.0%)
parse_rdn_val_title: 2 stmts out of 2 (100.0%)
parse_rdn_val_x520name: 2 stmts out of 2 (100.0%)
parse_sig_generic: 12 stmts out of 12 (100.0%)
parse_x509_Extension: 59 stmts out of 59 (100.0%)
parse_x509_Extension: 60 stmts out of 60 (100.0%)
parse_x509_tbsCertificate: 136 stmts out of 137 (99.3%)
parse_rdn_val_dc: 70 stmts out of 71 (98.6%)
parse_x509_Validity: 69 stmts out of 70 (98.6%)
......@@ -54,9 +54,9 @@ parse_GeneralSubtrees: 34 stmts out of 35 (97.1%)
parse_UserNotice: 33 stmts out of 34 (97.1%)
parse_ext_CRLDP: 33 stmts out of 34 (97.1%)
parse_ext_IAN: 33 stmts out of 34 (97.1%)
parse_x509_AlgorithmIdentifier: 32 stmts out of 33 (97.0%)
parse_UTCTime: 63 stmts out of 65 (96.9%)
parse_nine_bit_named_bit_list: 63 stmts out of 65 (96.9%)
parse_x509_AlgorithmIdentifier: 31 stmts out of 32 (96.9%)
parse_printable_string: 30 stmts out of 31 (96.8%)
find_alg_by_oid: 29 stmts out of 30 (96.7%)
find_dn_by_oid: 29 stmts out of 30 (96.7%)
......@@ -85,7 +85,7 @@ parse_OID: 40 stmts out of 43 (93.0%)
parse_GeneralName: 87 stmts out of 94 (92.6%)
parse_CPSuri: 12 stmts out of 13 (92.3%)
parse_policyQualifierInfo: 48 stmts out of 52 (92.3%)
parse_x509_subjectPublicKeyInfo: 35 stmts out of 38 (92.1%)
parse_x509_subjectPublicKeyInfo: 36 stmts out of 39 (92.3%)
parse_DistributionPoint: 69 stmts out of 75 (92.0%)
parse_sig_ecdsa: 46 stmts out of 50 (92.0%)
parse_algoid_params_generic: 11 stmts out of 12 (91.7%)
......@@ -96,13 +96,13 @@ find_curve_by_oid: 27 stmts out of 30 (90.0%)
_parse_arc: 32 stmts out of 36 (88.9%)
parse_ext_bad_oid: 8 stmts out of 9 (88.9%)
check_printable_string: 31 stmts out of 35 (88.6%)
parse_AttributeTypeAndValue: 31 stmts out of 35 (88.6%)
parse_x509_Extensions: 46 stmts out of 52 (88.5%)
parse_AttributeTypeAndValue: 30 stmts out of 34 (88.2%)
parse_ext_keyUsage: 30 stmts out of 34 (88.2%)
parse_algoid_params_ecdsa_with: 7 stmts out of 8 (87.5%)
parse_ia5_string: 27 stmts out of 31 (87.1%)
parse_DisplayText: 36 stmts out of 42 (85.7%)
parse_RelativeDistinguishedName: 24 stmts out of 28 (85.7%)
parse_explicit_id_len: 22 stmts out of 26 (84.6%)
parse_x509_signatureValue: 16 stmts out of 19 (84.2%)
get_identifier: 25 stmts out of 30 (83.3%)
parse_x509_signatureValue: 15 stmts out of 18 (83.3%)
......@@ -84,7 +84,7 @@ Potential entry points (2)
Global metrics
==============
Sloc = 3120
Sloc = 3125
Decision point = 677
Global variables = 190
If = 634
......
src/x509-parser.c:9238:[kernel:typing:incompatible-types-call] warning: expected 'char *' but got argument of type 'u8 *': buf
src/x509-parser.c:9242:[kernel:typing:incompatible-types-call] warning: expected 'char *' but got argument of type 'u8 *': buf
[kernel] warning: 1 state in saved file ignored. It is invalid in this Frama-C configuration.
[wp] warning: Missing RTE guards
src/x509-parser.c:9051:[wp] warning: \valid_function not yet implemented
src/x509-parser.c:9054:[wp] warning: \valid_function not yet implemented
(\valid_function(sig_alg->parse_sig))
src/x509-parser.c:9238:[wp] warning: Cast with incompatible pointers types (source: uint8*) (target: sint8*)
src/x509-parser.c:9242:[wp] warning: Cast with incompatible pointers types (source: uint8*) (target: sint8*)
FRAMAC_SHARE/libc/__fc_builtin.h:38:[wp] warning: Memory model hypotheses for function 'Frama_C_make_unknown':
/*@
behavior wp_typed:
......@@ -10,7 +10,7 @@ FRAMAC_SHARE/libc/__fc_builtin.h:38:[wp] warning: Memory model hypotheses for fu
requires \separated(p + (0 .. l - 1), &Frama_C_entropy_source);
*/
extern void Frama_C_make_unknown(char *p, size_t l);
src/x509-parser.c:9232:[wp:pedantic-assigns] warning: No 'assigns' specification for function 'main'.
src/x509-parser.c:9236:[wp:pedantic-assigns] warning: No 'assigns' specification for function 'main'.
Callers assumptions might be imprecise.
src/x509-parser.c:1876:[wp:pedantic-assigns] warning: No \from specification for assigned pointer 'param->curve_param'.
Callers assumptions might be imprecise.
......@@ -63,32 +63,32 @@ static int parse_x509_AlgorithmIdentifier(u8 const *buf, u16 len,
alg_param *param, u16 *eaten);
src/x509-parser.c:3487:[wp:pedantic-assigns] warning: No 'assigns \result \from ...' specification for function 'find_dn_by_oid'returning pointer type.
Callers assumptions might be imprecise.
src/x509-parser.c:4386:[wp] warning: Memory model hypotheses for function 'parse_x509_subjectPublicKeyInfo':
src/x509-parser.c:4387:[wp] warning: Memory model hypotheses for function 'parse_x509_subjectPublicKeyInfo':
/*@
behavior wp_typed:
requires \separated(buf + (..), (_alg_id const **)known_algs + (..));
requires \separated(eaten, (_alg_id const **)known_algs + (..));
*/
static int parse_x509_subjectPublicKeyInfo(u8 const *buf, u16 len, u16 *eaten);
src/x509-parser.c:7194:[wp:pedantic-assigns] warning: No 'assigns \result \from ...' specification for function 'find_kp_by_oid'returning pointer type.
src/x509-parser.c:7196:[wp:pedantic-assigns] warning: No 'assigns \result \from ...' specification for function 'find_kp_by_oid'returning pointer type.
Callers assumptions might be imprecise.
src/x509-parser.c:8065:[wp:pedantic-assigns] warning: No 'assigns \result \from ...' specification for function 'find_ext_by_oid'returning pointer type.
src/x509-parser.c:8067:[wp:pedantic-assigns] warning: No 'assigns \result \from ...' specification for function 'find_ext_by_oid'returning pointer type.
Callers assumptions might be imprecise.
src/x509-parser.c:8108:[wp:pedantic-assigns] warning: No \from specification for assigned pointer '*(parsed_oid_list +
src/x509-parser.c:8110:[wp:pedantic-assigns] warning: No \from specification for assigned pointer '*(parsed_oid_list +
(0 ..
sizeof(known_ext_oids) /
sizeof(known_ext_oids[0])
- 1))'.
Callers assumptions might be imprecise.
src/x509-parser.c:8178:[wp:pedantic-assigns] warning: No \from specification for assigned pointer '*(parsed_oid_list +
src/x509-parser.c:8180:[wp:pedantic-assigns] warning: No \from specification for assigned pointer '*(parsed_oid_list +
(0 ..
sizeof(known_ext_oids) /
sizeof(known_ext_oids[0])
- 1))'.
Callers assumptions might be imprecise.
src/x509-parser.c:8489:[wp:pedantic-assigns] warning: No \from specification for assigned pointer '*sig_alg'.
src/x509-parser.c:8492:[wp:pedantic-assigns] warning: No \from specification for assigned pointer '*sig_alg'.
Callers assumptions might be imprecise.
src/x509-parser.c:8491:[wp] warning: Memory model hypotheses for function 'parse_x509_tbsCertificate':
src/x509-parser.c:8494:[wp] warning: Memory model hypotheses for function 'parse_x509_tbsCertificate':
/*@
behavior wp_typed:
requires \separated(buf + (..), (_alg_id const **)known_algs + (..));
......@@ -98,7 +98,7 @@ src/x509-parser.c:8491:[wp] warning: Memory model hypotheses for function 'parse
*/
static int parse_x509_tbsCertificate(u8 const *buf, u16 len,
_alg_id const **sig_alg, u16 *eaten);
src/x509-parser.c:8821:[wp] warning: Memory model hypotheses for function 'parse_x509_signatureAlgorithm':
src/x509-parser.c:8824:[wp] warning: Memory model hypotheses for function 'parse_x509_signatureAlgorithm':
/*@
behavior wp_typed:
requires \separated(buf + (..), (_alg_id const **)known_algs + (..));
......
......@@ -2418,7 +2418,7 @@ static int parse_x509_AlgorithmIdentifier(const u8 *buf, u16 len,
buf += oid_len;
param_len = data_len - oid_len;
/*@ assert talg->parse_algoid_params \in { parse_algoid_params_generic, parse_algoid_params_ecdsa_with, parse_algoid_params_ecPublicKey, parse_algoid_params_rsa }; @*/
/*@ calls parse_algoid_params_generic, parse_algoid_params_ecdsa_with, parse_algoid_params_ecPublicKey, parse_algoid_params_rsa; @*/
ret = talg->parse_algoid_params(buf, param_len, param);
if (ret) {
......@@ -3591,6 +3591,7 @@ static int parse_AttributeTypeAndValue(const u8 *buf, u16 len, u16 *eaten)
* Let's now check the value associated w/ and
* following the OID has a valid format.
*/
/*@ assert cur->parse_rdn_val \in { parse_rdn_val_cn, parse_rdn_val_org, parse_rdn_val_org_unit, parse_rdn_val_title, parse_rdn_val_dn_qual, parse_rdn_val_pseudo, parse_rdn_val_dc, parse_rdn_val_x520name, parse_rdn_val_serial, parse_rdn_val_country, parse_rdn_val_locality, parse_rdn_val_state }; @*/
/*@ calls parse_rdn_val_cn, parse_rdn_val_x520name,
parse_rdn_val_serial, parse_rdn_val_country,
parse_rdn_val_locality, parse_rdn_val_state,
......@@ -4439,6 +4440,7 @@ static int parse_x509_subjectPublicKeyInfo(const u8 *buf, u16 len, u16 *eaten)
goto out;
}
/*@ assert alg->parse_subjectpubkey \in { parse_subjectpubkey_ec, parse_subjectpubkey_rsa } ; @*/
/*@ calls parse_subjectpubkey_ec, parse_subjectpubkey_rsa ; @*/
ret = alg->parse_subjectpubkey(buf, remain, &param);
if (ret) {
......@@ -8050,7 +8052,7 @@ static const _ext_oid known_ext_oids[] = {
/*
* We limit the amount of extensions we accept per certificate. This can be
* done because each kind of extension is allowed to appear only once in a
* given certificate. Note that it is logical to allow
* given certificate. Note that it is logical to allow
*/
#define MAX_EXT_NUM_PER_CERT NUM_KNOWN_EXT_OIDS
......@@ -8310,6 +8312,7 @@ static int parse_x509_Extension(const u8 *buf, u16 len,
}
/* Parse the parameters for that extension */
/*@ assert ext->parse_ext_params \in { parse_ext_AIA, parse_ext_AKI, parse_ext_SKI, parse_ext_keyUsage, parse_ext_certPolicies, parse_ext_policyMapping, parse_ext_SAN, parse_ext_IAN, parse_ext_subjectDirAttr, parse_ext_basicConstraints, parse_ext_nameConstraints, parse_ext_policyConstraints, parse_ext_EKU, parse_ext_CRLDP, parse_ext_inhibitAnyPolicy, parse_ext_bad_oid }; @*/
/*@ calls parse_ext_AIA, parse_ext_AKI, parse_ext_SKI, parse_ext_keyUsage, parse_ext_certPolicies, parse_ext_policyMapping, parse_ext_SAN, parse_ext_IAN, parse_ext_subjectDirAttr, parse_ext_basicConstraints, parse_ext_nameConstraints, parse_ext_policyConstraints, parse_ext_EKU, parse_ext_CRLDP, parse_ext_inhibitAnyPolicy, parse_ext_bad_oid ; @*/
ret = ext->parse_ext_params(buf, ext_data_len, critical, ctx);
if (ret) {
......@@ -9079,6 +9082,7 @@ static int parse_x509_signatureValue(const u8 *buf, u16 len,
goto out;
}
/*@ assert sig_alg->parse_sig \in { parse_sig_ecdsa, parse_sig_generic }; @*/
/*@ calls parse_sig_ecdsa, parse_sig_generic; @*/
ret = sig_alg->parse_sig(buf, len, eaten);
if (ret) {
......
......@@ -14,7 +14,11 @@
#include <unistd.h>
#include <string.h>
#if defined(__FRAMAC__)
#define ATTRIBUTE_UNUSED
#else
#define ATTRIBUTE_UNUSED __attribute__((unused))
#endif
typedef uint8_t u8;
typedef uint16_t u16;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment