vmpu_acl_stack does not halt if unsigned integer overflow occurs

**_Summary**_: Due to unsigned integer overflow, it is possible for the uVisor to fulfil a request for a larger amount of stack/context than is available.

Found using CBMC.
## Description

The procedure `vmpu_acl_stack` (in `core/system/src/mpu/vmpu_armv7.c`) allocates a protected stack/context for a given `box_id`, `context_size` and `stack_size`. Regions are allocated in the `bss_boxes` memory space.

We check that the procedure HALTs if the number of bytes requested is greater-than the number of allocatable bytes in bss_boxes:

```
nbytes_allocatable < nbytes_requested
```
- where `nbytes_allocatable = bss_boxes_end - g_box_mem_pos`
- and `nbytes_requested = context_size + stack_size`

Consider the following scenario where we expect a HALT to occur:

```
nbytes_allocatable = 0x001c1050
nbytes_requested = 0x20006000
```

However, the procedure pads the memory request by computing (line 572):

```
((nbytes_requested * 8) / 6)
```

In this case we overflow when we multiply-by 8 (shift-left by 3). If we had 64-bit arithmetic, we would get the correct answer (0x2aab2aaa) but with overflow we get (0x8000), which is less than nbytes_allocatable. Consequently, the procedure does not fail its out-of-memory check and it proceeds to allocates a smaller buffer size for the box than it requested. That is, the expected HALT does not occur.
## Files

Can be found in the review repo under `issues/vmpu_acl_stack_overflow`.
- `check_vmpu_acl_stack.c` -- top-level testbench
- `tb_common.{h,c}` -- testbench utilities
- `run_cbmc.sh` -- script to invoke model checker
- `cex.txt` -- example counterexample output
## Reproducing

Requires:
- testbench files as above
- cbmc installed and on path
- `$UVISOR` environment variable setup to point to local copy of uVisor repo

``` bash
$ ./run-cbmc.sh check_vmpu_acl_stack.c tb_common.c --ILP32 --stop-on-fail -DCEX_PRINTING | tee cex.txt && grep ">" cex.txt
```

This will produce a counterexample in [cex.txt] and a summary. This will be something like:

```
> halt_must_occur = 1
> box_id = 4
> context_size = 2139070464
> stack_size = 8437760
> allocatable_nbytes = 4208577
> box_request_nbytes = 2147508224
> procedure finished without halting
> procedure allocated 46529 bytes
```

To see that overflows due to padding are the cause of the problem:

``` bash
$ ./run-cbmc.sh check_vmpu_acl_stack.c tb_common.c --ILP32 --stop-on-fail -DASSUME_NO_OVERFLOW
```

This adds assumptions (constraints) to the size of `nbytes_requested` to ensure that no overflow is possible.

[cex.txt](https://github.com/ARMmbed/uvisor/files/373243/cex.txt)

Start in core/system/src/mpu/vmpu_armv7.c at the vmpu_acl_stack padding calculation around line 572. Run run-cbmc.sh with check_vmpu_acl_stack.c and tb_common.c using the reproducer and compare with the ASSUME_NO_OVERFLOW run. Done means the out-of-memory case halts instead of allocating a smaller buffer, with the counterexample no longer reproducible.

Written by the indexing model from the issue text.