SMT2 formal verification of security-critical code paths
Entity expansion depth ≤ 40 to prevent billion-laughs attacks. From xmlStringLenDecodeEntities() in parser.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun depth () Int)
(assert
(<= depth 40))
(assert
(>= depth 0))
(assert
(or (< depth 0) (> depth 40)))
(check-sat)
Attribute count per element bounded. From xmlParseStartTag2() in parser.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun nb_attributes () Int)
(assert
(<= nb_attributes 10000))
(assert
(>= nb_attributes 0))
(assert
(or (< nb_attributes 0) (> nb_attributes 10000)))
(check-sat)
Element/attribute name length bounded. From xmlParseName() in parser.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun name_len () Int)
(assert
(<= name_len 50000))
(assert
(>= name_len 1))
(assert
(or (< name_len 1) (> name_len 50000)))
(check-sat)
Namespace URI length bounded to prevent memory exhaustion. From xmlParseStartTag2().
; benchmark generated from python API
(set-info :status unknown)
(declare-fun ns_uri_len () Int)
(assert
(<= ns_uri_len 8192))
(assert
(>= ns_uri_len 1))
(assert
(or (< ns_uri_len 1) (> ns_uri_len 8192)))
(check-sat)
Encoding declaration length bounded. From xmlParseEncodingDecl() in parser.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun encoding_decl_len () Int)
(assert
(<= encoding_decl_len 40))
(assert
(>= encoding_decl_len 1))
(assert
(or (< encoding_decl_len 1) (> encoding_decl_len 40)))
(check-sat)
Entity value length bounded by XML_MAX_TEXT_LENGTH to prevent memory bomb via large inline entities. From xmlParseEntityValue() in parser.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun entity_value_len () Int)
(assert
(<= entity_value_len 10000000))
(assert
(>= entity_value_len 0))
(assert
(or (< entity_value_len 0) (> entity_value_len 10000000)))
(check-sat)
Comment content length bounded by XML_MAX_TEXT_LENGTH to prevent memory exhaustion via giant comments. From xmlParseCommentComplex() in parser.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun comment_len () Int)
(assert
(<= comment_len 10000000))
(assert
(>= comment_len 0))
(assert
(or (< comment_len 0) (> comment_len 10000000)))
(check-sat)
PI target name length bounded by XML_MAX_NAME_LENGTH to prevent dictionary interning exhaustion via oversized processing instruction names. From xmlParsePITarget() in parser.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun pi_target_name_len () Int)
(assert
(<= pi_target_name_len 50000))
(assert
(>= pi_target_name_len 1))
(assert
(or (< pi_target_name_len 1) (> pi_target_name_len 50000)))
(check-sat)
PI content length bounded by XML_MAX_TEXT_LENGTH to prevent memory exhaustion via oversized processing instruction content. From xmlParsePI() in parser.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun pi_content_len () Int)
(assert
(<= pi_content_len 10000000))
(assert
(>= pi_content_len 0))
(assert
(or (< pi_content_len 0) (> pi_content_len 10000000)))
(check-sat)
CDATA section length bounded by XML_MAX_TEXT_LENGTH to prevent memory exhaustion via oversized CDATA sections. From xmlParseCDSect() in parser.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun cdata_section_len () Int)
(assert
(<= cdata_section_len 10000000))
(assert
(>= cdata_section_len 0))
(assert
(or (< cdata_section_len 0) (> cdata_section_len 10000000)))
(check-sat)
PubidLiteral length bounded by XML_MAX_NAME_LENGTH to prevent oversized public identifiers in DTD PUBLIC declarations. From xmlParsePubidLiteral() in parser.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun pubid_literal_len () Int)
(assert
(<= pubid_literal_len 50000))
(assert
(>= pubid_literal_len 1))
(assert
(or (< pubid_literal_len 1) (> pubid_literal_len 50000)))
(check-sat)
Notation name length bounded by XML_MAX_NAME_LENGTH to prevent oversized notation names in DTD NOTATION declarations. From xmlParseNotationDecl() in parser.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun notation_name_len () Int)
(assert
(<= notation_name_len 50000))
(assert
(>= notation_name_len 1))
(assert
(or (< notation_name_len 1) (> notation_name_len 50000)))
(check-sat)
Attribute default value length bounded by XML_MAX_TEXT_LENGTH to prevent memory exhaustion via oversized default values in DTD ATTLIST declarations. From xmlParseAttValueInternal() in parser.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun attvalue_default_len () Int)
(assert
(<= attvalue_default_len 10000000))
(assert
(>= attvalue_default_len 0))
(assert
(or (< attvalue_default_len 0) (> attvalue_default_len 10000000)))
(check-sat)
SystemLiteral length bounded by XML_MAX_NAME_LENGTH to prevent oversized external IDs in DTD SYSTEM/PUBLIC declarations. From xmlParseSystemLiteral() in parser.c.
; benchmark generated from python API
(set-info :status unknown)
(declare-fun system_literal_len () Int)
(assert
(<= system_literal_len 50000))
(assert
(>= system_literal_len 1))
(assert
(or (< system_literal_len 1) (> system_literal_len 50000)))
(check-sat)