Strengthening Verification

A problem with verifying int_stack is that there is not enough state to check whether it really has not been modified. For instance, a buggy pointer could cause any of the values that had been pushed onto the stack to be changed, and the verify_int_stack() routine would not catch it.

Occasionally, we need more integrity checking. This usually arises when:

One approach to ensuring complete integrity checking is to compute some kind of checksum or signature. A checksum is a small value, usually 8 to 32 bit, that is added to the ADT, and is computed using the contents of the rest of the data structure. Another way of looking at the checksum is that it is a hash of the data structure.

The checksum usually has two requirements:

For the int_stack ADT, a decent checksum is to xor (^) all the elements of the data structure. This will result in the following header:


	struct int_stack {
	  /* other stuff ... */
	  unsigned	is_chksum;
	};
	/* other accessor macros ... */
	#define x_chksum_int_stack(_s)	(deref_int_stack(_s)->is_chksum)

Verification involves recomputing the checksum and ensuring that it matches.


	void
	verify_int_stack(
		FILE *		file,
		int		line,
		const int_stack	stack
		)
	{
	  unsigned	chksum;
	  int		i;

	  /* other verifys ...*/
	  chksum = (unsigned)len_int_stack(stack);
	  chksum ^= (unsigned)max_int_stack(stack);
	  chksum ^= (unsigned)vals_int_stack(stack);
	  for( i = 0; i < len_int_stack(stack); i++ ) {
	    chksum ^= (unsigned)vals_int_stack(stack)[i];
	  }
	  verify(file, line, chksum == x_chksum_int_stack(stack));
	}

We will also have to modify the various functions to setup the checksum appropriately. Here, we show the ones most affected.


	int_stack
	make_int_stack(void)
	{
	  int_stack	stack = xalloc(struct int_stack);
	  unsigned	chksum;

	  x_max_int_stack(stack) = 16;
	  x_len_int_stack(stack) = 0;
	  x_vals_int_stack(stack) = xnalloc(int, 16);

	  chksum = (unsigned)len_int_stack(stack);
	  chksum ^= (unsigned)max_int_stack(stack);
	  chksum ^= (unsigned)vals_int_stack(stack);
	  x_chksum_int_stack(stack) = chksum;

	  VERIFY_INT_STACK(stack);
	  return stack;
	}

	void
	push_int_stack(
		int_stack	stack,
		int		val
		)
	{
	  int	len = len_int_stack(stack);
	  int	max = max_int_stack(stack);
	  int	nmax;
	  int *	vals;
	  int *	nvals;
	  int	i;

	  VERIFY_INT_STACK(stack);

	  if( len == max ) {
	    nmax = max + 16;
	    nvals = xnalloc(int, nmax);
	    vals = vals_int_stack(stack);
	    for( i = 0; i < len; i++ ) {
	      nvals[i] = vals[i];
	    }
	    x_max_int_stack(stack) = nmax;
	    x_vals_int_stack(stack) = nvals;
	    xnfree(int, max, vals);

	    /* undo the old values */
	    x_chksum_int_stack(stack) ^= (unsigned)vals;
	    x_chksum_int_stack(stack) ^= (unsigned)max;

	    /* update the new values */
	    x_chksum_int_stack(stack) ^= (unsigned)nvals;
	    x_chksum_int_stack(stack) ^= (unsigned)nmax;
	  }

	  vals_int_stack(stack)[len] = val;
	  x_len_int_stack(stack) = len+1;

	  /* undo the old values */
	  x_chksum_int_stack(stack) ^= (unsigned)len;

	  /* update the new values */
	  x_chksum_int_stack(stack) ^= (unsigned)(len+1);
	  x_chksum_int_stack(stack) ^= val;

	  VERIFY_INT_STACK(stack);
	}

	void
	pop_int_stack(
		int_stack	stack
		)
	{
	  int	len = len_int_stack(stack);
	  VERIFY_INT_STACK(stack);

	  x_len_int_stack(stack)--;

	  /* undo the old values in the checksum */
	  x_chksum_int_stack(stack) ^= (unsigned) len;
	  x_chksum_int_stack(stack) ^= (unsigned) vals_int_stack(len)[len-1];
	  /* update the checksum with new value */
	  x_chksum_int_stack(stack) ^= (unsigned) (len-1);

	  VERIFY_INT_STACK(stack);
	}

Note that a fair bit of code has been added to the routines for checksum computation. This is because of run-time efficiency. Alternatively, we could define a function that recomputed the checksum, and call that prior to exiting the functions that modify the data structure.


	static void
	update_checksum_int_stack(
		int_stack	stack
		)
	{
	  unsigned	chksum;
	  int		i;

	  chksum = (unsigned)len_int_stack(stack);
	  chksum ^= (unsigned)max_int_stack(stack);
	  chksum ^= (unsigned)vals_int_stack(stack);
	  for( i = 0; i < len_int_stack(stack); i++ ) {
	    chksum ^= (unsigned)vals_int_stack(stack)[i];
	  }
	  x_chksum_int_stack(stack) = chksum;
	}

	void
	pop_int_stack(
		int_stack	stack
		)
	{
	  VERIFY_INT_STACK(stack);

	  x_len_int_stack(stack)--;

	  update_checksum_int_stack(stack);
	  VERIFY_INT_STACK(stack);
	}


Next Prev Main Top Feedback