Security vulnerabilities (possible overflows) in helper functions of Beacon Chain

[franck44]

Some overflows may happen in several helper functions of the Beacon Chain.
This results in security vulnerabilities CWE-190, integer overflow.

How the problem was discovered?

As part of the formal verification of the Eth2.0 specification in Dafny project.

Detailed analysis, fixes and correctness proofs of the fixes.

Detailed analysis and fixes reported as issue 45 of the eth2.0-dafny project.
Correctness formal proofs of the fixes have been established using Dafny 2.3.0.

Possible overflow in assert statement in get_block_root_at_slot

The following code snippet contains a assert statement that may result in an overflow:

def get_block_root_at_slot(state: BeaconState, slot: Slot) -> Root:
    """
    Return the block root at a recent ``slot``.
    """
    assert slot < state.slot <= slot + SLOTS_PER_HISTORICAL_ROOT  
    return state.block_roots[slot % SLOTS_PER_HISTORICAL_ROOT]

note: the above assert is not a pre-condition to guarantee the absence of array-out-of-bounds error when dereferencing state.block_roots (this never happens because block_roots has size SLOTS_PER_HISTORICAL_ROOT) but a functional property of the system (requesting the block root for a slot that is too far in the past should not be permitted).

The pre-condition of the previous function should be strengthened to prevent slot + SLOTS_PER_HISTORICAL_ROOT from overflowing i.e. assert(slot as int + SLOTS_PER_HISTORICAL_ROOT as int < 0x10000000000000000) where
0x10000000000000000 is max(unit64) + 1.

### Possible overflow in `compute_start_slot_at_epoch`
Because `Epoch` ranges over `uint64`, the multiplication can overflow in the following code snippet:
```python
def compute_start_slot_at_epoch(epoch: Epoch) -> Slot:
    """
    Return the start slot of ``epoch``.
    """
    return Slot(epoch * SLOTS_PER_EPOCH)

The pre-condition should be strengthened to epoch as int * SLOTS_PER_EPOCH as int < 0x10000000000000000

Other functions impacted by the previous strengthening of pre-conditions

As a result functions calling compute_start_slot_at_epoch or get_block_root_at_slot should have their pre-conditions strengthened.
This includes get_block_root

def get_block_root(state: BeaconState, epoch: Epoch) -> Root:
    """
    Return the block root at the start of a recent ``epoch``.
    """
    return get_block_root_at_slot(state, compute_start_slot_at_epoch(epoch))

the pre-conditions of should be:

function method get_block_root(state: BeaconState, epoch: Epoch) : Root    
     requires state.slot as int + SLOTS_PER_HISTORICAL_ROOT as int < 0x10000000000000000 // Max(uint64) + 1
     requires epoch as int * SLOTS_PER_EPOCH as int < 0x10000000000000000   
     requires compute_start_slot_at_epoch(epoch) < state.slot <= compute_start_slot_at_epoch(epoch) + SLOTS_PER_HISTORICAL_ROOT  
{ 
        var e := compute_start_slot_at_epoch(epoch);
        get_block_root_at_slot(state, e)
}

Conclusion

The proposed strengthening of pre-conditions in the previous functions guarantee the absence of overflows in all of them.