From owner-freebsd-hackers@FreeBSD.ORG  Sat Feb 21 10:26:16 2004
Return-Path: <owner-freebsd-hackers@FreeBSD.ORG>
Delivered-To: freebsd-hackers@freebsd.org
Received: from mx1.FreeBSD.org (mx1.freebsd.org [216.136.204.125])
	by hub.freebsd.org (Postfix) with ESMTP
	id 32A7316A4CE; Sat, 21 Feb 2004 10:26:16 -0800 (PST)
Received: from mx01.netapp.com (mx01.netapp.com [198.95.226.53])
	by mx1.FreeBSD.org (Postfix) with ESMTP
	id 28A0B43D1D; Sat, 21 Feb 2004 10:26:16 -0800 (PST)
	(envelope-from kmacy@netapp.com)
Received: from frejya.corp.netapp.com (frejya [10.57.157.119])
	i1LIQFJC013691;	Sat, 21 Feb 2004 10:26:15 -0800 (PST)
Received: from siml2-fe.eng.netapp.com (siml2-fe.eng.netapp.com [10.56.9.152])
	i1LIQEB5002969;	Sat, 21 Feb 2004 10:26:14 -0800 (PST)
Date: Sat, 21 Feb 2004 10:26:14 -0800 (PST)
From: Kip Macy <kmacy@netapp.com>
X-X-Sender: kmacy@siml2.eng.netapp.com
To: Robert Watson <rwatson@freebsd.org>
In-Reply-To: <Pine.NEB.3.96L.1040221131348.70781V-100000@fledge.watson.org>
Message-ID: <Pine.LNX.4.44.0402211019001.8075-100000@siml2.eng.netapp.com>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
cc: hackers@freebsd.org
cc: Ted Unangst <tedu@coverity.com>
Subject: Re: use after free bugs
X-BeenThere: freebsd-hackers@freebsd.org
X-Mailman-Version: 2.1.1
Precedence: list
List-Id: Technical Discussions relating to FreeBSD
	<freebsd-hackers.freebsd.org>
List-Unsubscribe: <http://lists.freebsd.org/mailman/listinfo/freebsd-hackers>,
	<mailto:freebsd-hackers-request@freebsd.org?subject=unsubscribe>
List-Archive: <http://lists.freebsd.org/pipermail/freebsd-hackers>
List-Post: <mailto:freebsd-hackers@freebsd.org>
List-Help: <mailto:freebsd-hackers-request@freebsd.org?subject=help>
List-Subscribe: <http://lists.freebsd.org/mailman/listinfo/freebsd-hackers>,
	<mailto:freebsd-hackers-request@freebsd.org?subject=subscribe>
X-List-Received-Date: Sat, 21 Feb 2004 18:26:16 -0000

> 
> I wonder if the same approach relating to memory allocation and free
> checking via static analysis could be applied to locking and unlocking of
> locks?  I.e.:

Yes. See Dawson's papers. That is one of the examples given. Use after free is 
one of the stock checkers. I don't think that there is a stock checker for 
locks, it might be harder to infer lock/unlock then malloc/free. In which case 
one would have to write an application specific lock check. In addition, in the
case of nested locks, the FSA used wouldn't suffice and one would have to call 
out to C code. The first two are easy - I'd have to look at the MetaL manual to
figure out how difficult the third one is.

> 
> - We don't release locks more than once.
> 
> - We don't forget to unlock.
> 
> - We hold a lock before accessing certain fields (defined by annotation)
>   of a structure.



			-Kip