Tracing secure information flow through mode changes

Communications devices intended for use in security- critical applications must be rigorously evaluated to ensure they preserve data confidentiality. This pro- cess includes tracing the flow of classified informa- tion through the device's circuitry. Previous work has shown how this can be done using graph analysis techniques for each of the device's distinct operating modes. However, such analyses overlook potential in- formation flow between modes, via components that store information in one mode and release it in an- other. Here we show how graph-based analyses can be extended to allow for information flow through se- quences of consecutive modes.