[C-safe-secure-studygroup] Enforcement and guidance

[Roberto Bagnara]

I would like to attempt a mild formalization that might help to
understand what are we trying to achieve.  I hope this can contribute
to clarity of objectives and means.

We have two categories: the undesired behaviors and the checkers.
The first category, undesired behaviors, is populated by entities that
are characterized by a single attribute, UNDB:

    UNDB: What we want to avoid.

The second category, checkers, contains entities that are characterized
by two attributes, CHCK and PREC:

    CHCK: What we choose to check.
    PREC: The precision of implementation with respect to CHCK.
          This, in turn, is given by the combination of two Boolean
          attributes FPOS and FNEG.  So PREC has 4 possible values:

          !FPOS && !FNEG: exact
           FPOS && !FNEG: complete
          !FPOS &&  FNEG: best-effort TWM (three wise monkeys)
           FPOS &&  FNEG: best-effort

In general, for each undesired behavior there can be several checks.
In order to simplify things, here I only consider checks that, alone,
do cover an undesired behavior.  For a check to cover an undesired
behavior I mean

    !CHCK --> !UNDB

that is, if CHCK finds nothing, then UNDB cannot happen.
Note that, while UNDB may correspond to a complex program property
(very often an undecidable one), CHCK can correspond to a simpler
program property (which may even be decidable on the entire language
or for the relevant subset of the language).

Here is an example:

    UNDB == After an allocated block of dynamic storage has been
            deallocated by a memory management function, the evaluation
            of any pointers into the freed memory, including being
            dereferenced or acting as an operand of an arithmetic
            operation, type cast, or right-hand side of an assignment,
            shall be diagnosed.

    checker1: (syntactic analysis of any kind, even cpp + grep)
      CHCK1 == the program does not contain any reference to free()
      PREC1 == exact (meaning that it is possible to implement the
               check in an exact way)

    checker2: (any analysis algorithm)
      CHCK2 == the program does not contain a call to free() in a
               feasible execution path
      PREC2 != exact (meaning that it is not possible to implement the
               check in an exact way)

    checker3: (syntactic analysis based on AST visit)
      CHCK3 == the program implements and systematically uses a smart
               pointer class that ensures all pointers to an allocated
               block of dynamic storage are zeroed immediately after
               deallocation
      PREC3 == exact

    checker4: (as implemented in Clang static analyzer)
      CHCK4 == UNDB
      PREC4 == best-effort

    checker5: (any sound abstract interpreter)
      CHCK5 == UNDB
      PREC5 == complete

    checker6: (time-limited valgrind run of the real program
               with feasible inputs)
      CHCK6 == UNDB
      PREC6 == best-effort TWM

In a truly critical industrial sector, what people needs is to exclude
all undesired behaviors from a program: those that cannot be excluded
automatically will have to be excluded manually.  The ideal situation
for them is to have a collection of checkers that do not have false
negatives and that do not give any report for the program considered:
this proves the undesired behaviors cannot happen.  When different
checks are available, they will choose those that require a level
of discipline that is compatible with their other objectives.
In these sectors CHCK != UNDB is both desirable and acceptable.

In non-critical sectors some undesired behaviors might still be
acceptable and, typically, in such sectors people is much less
inclined to accept checks that require discipline on the part of
the programmers.  In these sectors there is a push to have CHCK == UNDB.

Now, what is our objective?  I take it for granted that our objective
is not to describe the set of undesired behaviors, i.e., writing
amplifications for all the items in C11's Annex J and all the items in CWE.
And, for the same reason, I take it for granted that we do not want
to have CHCK == UNDB for more than a few undesired behaviors for which
we really have no guidance to offer.  I also believe we should not
try do duplicate MISRA C: MISRA C represents a collection of checks
(strongly based on the idea of language subsetting) covering a wide
class of undesired behaviors that, in exchange for a lot of
discipline, provides rather strict guidance for the development of
safety-critical and security-critical systems, with an emphasis on
embedded systems.

I assume the original intent of TS 17961:2016, i.e., the one of serving
people outside the safety-critical community, has not changed:

    There are already standards that address safety-critical code and
    therefore security-critical code. The problem is that because they
    must focus on preventing essentially all bugs, they are required
    to be so strict that most people outside the safety-critical
    community do not want to use them.

If my assumptions are correct, then our objective is to identify
a set of checks that sits in the middle of what already exists,
i.e., which:

1) provides rule-based guidance on how to avoid undesired behaviors;
2) requires less discipline than, e.g., MISRA C, so as to be acceptable,
   at least in principle, to all C organizations writing even modestly
   critical code;
3) is amenable to implementations with low rates of false positives
   and false negatives.

It is a difficult task, but the team is an excellent one and I am
confident we will succeed.

Of course, my assumptions above may be completely wrong: I articulated
them to the best of my possibilities just as a contribution to the
group discussion.
Kind regards,

   Roberto

-- 
     Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                              BUGSENG srl - http://bugseng.com
                              mailto:roberto.bagnara at bugseng.com