seL4 / sel4test

Test suite for seL4.
http://sel4.systems
Other
24 stars 60 forks source link

Add tests for SMC Capability #85

Closed Furao closed 1 year ago

Furao commented 1 year ago

This new test will make sure that the SMC capability and its associated API call work as expected.

It tests the following:

  1. A correctly configured call works
  2. An SMC call with a function ID that uses a cap with a different badge fails
  3. Minting an SMC cap from an SMC cap with a badge other than 0 fails

I tested this with the following configuration:

../init-build.sh -DPLATFORM=zcu102 -DRELEASE=true -DARM_HYP=TRUE -DKernelAllowSMCCalls=true

I wanted to test on QEMU, but it turned out to be non-trivial to integrate ATF with QEMU for sel4Test. It is doable, but I don't have the bandwidth to support it.

Note: This test assumes you are running ATF in EL3 on an AARCH64 platform. The successful test checks the standard service version and it reports back 0.1 (See https://github.com/ARM-software/arm-trusted-firmware/blob/master/include/services/std_svc.h). Technically this could change in the future and break the test, however the version hasn't changed in the last 9 years since the service was written.

This test requires these PRs:

Furao commented 1 year ago

CI should probably be updated to include another test configuration on at least the zcu106 to enable KernelAllowSMCCalls.