← All specifications

CERT C/C++ Secure Coding — ponens Policy Pack

This pack maps the SEI CERT Coding Standards (CERT C and CERT C++, from Carnegie Mellon’s Software Engineering Institute) onto computable ponens policies. Unlike the category-based MISRA/JSF packs, CERT is built on a risk model, and that risk-prioritized remediation process is what this pack governs.

Source: SEI CERT C and CERT C++ Secure Coding Standards — https://wiki.sei.cmu.edu/confluence/display/seccode

Why this maps onto ponens (and why it’s not a MISRA clone)

CERT’s individual rules are checked by static analysis, so — as with MISRA and JSF — ponens does not re-encode them. What is distinctive about CERT, and what ponens governs here, is its risk assessment and prioritized remediation:

This is a risk-prioritized process, not a category process — genuinely different from MISRA’s Mandatory/Required/Advisory and JSF’s Shall/Will/Should. The same methodology covers CERT C and CERT C++, so this is one pack, not two.

CERTponens
The coding/security-analysis activity recordthe trace
A risk/remediation obligationa policy (temporal formula)
Rule violation / open L1 vs advisory departureerror (Red) / warning (Amber)

Trace model

Worked traces: examples/cert/governed.json (11/11 Green) and violating.json (6 Red + 3 Amber — including an assessed-but-unremediated L1 finding shipped at release). Run ponens trace check <file>.

The pack

errorRed; warningAmber.

Rules vs Recommendations (security)

PolicyFormulaRAG
cert_rule_violation_remediatedG(Finding ∧ cert_rule_violation → remediated ∨ deviation_approved)R
cert_recommendation_departure_recordedG(Finding ∧ cert_recommendation_departure → recorded)A

Risk Assessment (security)

PolicyFormulaRAG
cert_risk_assessedG(Finding → severity_assessed ∧ likelihood_assessed ∧ remediation_assessed)R
cert_priority_assignedG(Finding → priority_assigned)R

Prioritized Remediation — L1/L2/L3 (security)

PolicyFormulaRAG
cert_l1_remediatedG(level_l1 → remediated)R
cert_no_open_l1_at_releaseG(Release → ¬open_l1)R
cert_l2_reviewedG(level_l2 → reviewed)A

Verification & Enforcement (workflow)

PolicyFormulaRAG
cert_static_analysis_before_commitG(GitCommit → P(StaticAnalysis ∧ cert_ruleset))R
cert_undecidable_manual_reviewG(undecidable_violation → manual_review)A

Deviations & Records (auditability)

PolicyFormulaRAG
cert_deviation_documentedG(Deviation → rationale_recorded ∧ deviation_approved)R
cert_conformance_recordedG(Release → P(conformance_summary))R

Aggregation

ponens trace check aggregates the pack: any error fail ⇒ Red (an open L1 at release, an unremediated rule violation, a missing risk assessment, or no conformance record); else any warning fail ⇒ Amber (recommendation departures, L2 review, undecidable-rule review); else Green.

Scope note

This is the one new standard from the Polyspace coding-rule catalogue that adds a genuinely different model (risk-prioritized remediation). The other entries on that page — ISO/IEC TS 17961, AUTOSAR C++14 (now folded into MISRA C++:2023), and the MISRA version variants — are rulesets the existing MISRA/JSF compliance-process packs already parameterize over, so they are intentionally not separate packs. The 221+ individual CERT rules themselves are enforced by a CERT-checking static analyzer; this pack governs the risk/remediation process around its results.