Be Forgetful!

[gmhwxi]

Kiwamu cited the following security issue in his earlier message

>>Dear all,

>>There is a security issue on FreeBSD:

* Security Advisory:
https://www.freebsd.org/security/advisories/FreeBSD-SA-20:20.ipv6.asc
* The patch: https://github.com/freebsd/freebsd/commit/5707de0ed806712f53752acd433313a39f63f15c

Basically, someone wrote the following line:

error = ip6_pcbopts(&inp->in6p_outputopts,  m, so, sopt);

The code should have been written as follows:

INP_WLOCK(inp);
error = ip6_pcbopts(&inp->in6p_outputopts, m,  so, sopt);

INP_WUNLOCK(inp);

In other words, the spin lock attached to 'inp' needs to be grabbed first

to avoid a potential race condition.

Of course, this kind of bug can be readily detected if ip6_pcbopts is required

to take a proof argument (to show that the aforementioned spin lock is grabbed):

error = ip6_pcbopts(pf | &inp->in6p_outputopts, m,  so, sopt);

If you want to make sure that the grabbed lock is indeed the right one

for protecting 'inp', the type assigned to ip6_pcbopts is actually quite involved.

What I would like to say here is that you should probably try to be forgetful:

https://en.wikipedia.org/wiki/Forgetful_functor

A forgetful functor is a concept in category theory. It is really just a fancy word

to describe an act of ignoring details. For the ip6_pcbopts example, we know that

a proof of some sort is needed. And we don't have to get into details at this point:

pf = INP_WLOCK(inp);
error = ip6_pcbopts(pf | &inp->in6p_outputopts, m,  so, sopt);

INP_WUNLOCK(pf | inp);

We can introduce a (non-dependent) abstract view for the proof returned from calling INP_WLOCK. It is essential to keep it simple so that this approach can actually scale.

My very simple point is that

1) There are a lot of bugs out there

2) You rarely need the full rigor of ATS to uncover many of them

Trying to be forgetful can actually be a very successful strategy for handling

large code bases.

--Hongwei