Ensuring Secure Information Flow in Partially Reconfigurable Architectures by Means of Process Algebra Analysis

Field-programmable gate arrays (FPGAs) provide a means to massively parallelize computations. In order to make more efficient use of FPGA devices, the method of partial dynamic reconfiguration can be applied: By means of this approach, the FPGA configuration is updated at run-time so that the device can feature new functionality. If multiple stakeholders make use of the same device, it has to be ensured that confidential information cannot be leaked between these parties. Therefore, all feasible hazards of illicit information flow need to be taken into account. In this work, partial dynamic reconfiguration is scheduled using the π-calculus, a process algebra. Within the presented framework, a variant of the π- calculus is employed to activate and deactivate partial modules and to rearrange their interconnect. The modules employed by different stakeholders use ports for communication, for which valid targets of information flow can be defined. By means of formal verification, it is evaluated whether the information flow between functional units of the stakeholders proceeds according to the specification. Using a set of analysis rules, an associated tool can verify whether a given reconfiguration schedule ensures secure information flow.