Open nchong opened 8 years ago
ARM Internal Ref: IOTSFW-2853
This bug can also be triggered via vmpu_arch_init_hw
in vmpu_armv7m.c
when building the static acl for the sram. If the total size of the sram is very small (< 256 bytes) then an UNPREDICTABLE RASR will be generated. Fixing the problem in vmpu_acl_update_box_region
is the right place to fault though.
In the v7M architecture, it is UNPREDICTABLE to have a RASR value with a non-zero SRD field for a region of less than 256 bytes (B3-697 of ARM DDI 0403E.b). It is possible to create an UNPREDICTABLE RASR value that will be programmed into the MPU by the uVisor.
The procedure
vmpu_acl_update_box_region
is responsible for generating a RASR value to represent the ACL. However, no check is made to ensure the RASR is architecturally valid with respect to the condition above. In particular, consider the generated RASR for an ACL of size 32 bytes and a non-zero SRD.A sanity check should be added to check that all ACLs with non-zero SRD fields request 256 bytes or more. Should this be performed after rounding? Is an ACL requesting 200 bytes with round-up allowed to specify a non-zero SRD?
Found using CBMC.