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 -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/58f81db1-2d98-4779-8c37-fd8a8195e2bfn%40googlegroups.com.
