Problem Description:

Steps to a possible buffer_underflow bug in ib700wdt.c, function ibwdt_ioctl:

1. new margin is loaded using get_user(new_margin, p) in case WDIOC_SETTIMEOUT in the function ibwdt_ioctl. Important: assume that new_margin == 30
2. ibwdt_set_heartbeat(new_margin) is called
3. the check "if ((t < 0) || (t > 30))" in ibwdt_set_heartbeat is not going to fail because t == 30 (t is new_margin)
4. in the loop, the check wd_times[i] > t is never going to be true because none of the wd_times are greater than the value of t (i.e. 30)
5. we are exiting the loop with i == -1 and therefore setting wd_margin to -1 in the line wd_margin = i;
6. we are returning from ibwdt_set_heartbeat and wd_margin is -1
7. we fall through to case WDIOC_GETTIMEOUT
8. we access the wd_times array with wd_margin == -1 on line "return put_user(wd_times[wd_margin], p);"

I found this bug using my own static checker for low-level systems software whose codename is Smack, which I am developing as a part of my PhD. For the sake of my research (and also I am currently in the process of writing a paper about Smack), I would greatly appreciate if you could confirm/dispute the bug as soon as possible.

Thanks a lot!
-- Zvonimir


Furthermore, here are the pieces of code which are causing this buffer-underflow bug in ib700wdt.c:

static int wd_times[] = {
	30,	/* 0x0 */
	28,	/* 0x1 */
	26,	/* 0x2 */
	24,	/* 0x3 */
	22,	/* 0x4 */
	20,	/* 0x5 */
	18,	/* 0x6 */
	16,	/* 0x7 */
	14,	/* 0x8 */
	12,	/* 0x9 */
	10,	/* 0xA */
	8,	/* 0xB */
	6,	/* 0xC */
	4,	/* 0xD */
	2,	/* 0xE */
	0,	/* 0xF */
};

function ibwdt_ioctl:
.....
  case WDIOC_SETTIMEOUT:
    if (get_user(new_margin, p))
      return -EFAULT;
    if (ibwdt_set_heartbeat(new_margin))
      return -EINVAL;
    ibwdt_ping();
    /* Fall */

  case WDIOC_GETTIMEOUT:
    return put_user(wd_times[wd_margin], p);
.....

function ibwdt_set_heartbeat:
static int
ibwdt_set_heartbeat(int t)
{
	int i;

	if ((t < 0) || (t > 30))
		return -EINVAL;

	for (i = 0x0F; i > -1; i--)
		if (wd_times[i] > t)
			break;
	wd_margin = i;
	return 0;
}