Unpredictable changes to the environment of a cyber-physical system introduce the potential for unsafe operating conditions. Should components of an architecture be subject to cyber attacks, hardware failures, or adverse environmental conditions, it is important the safety-critical features still be functional to avoid dangerous conditions for users. Graceful degradation refers to systems where some components may experience failure, but the system maintains safety-critical features. The trust boundry of a system refers to the minimal set of components required before safety-critical features are sacrificed. Identifying trust boundaries and building systems with graceful degradation allow systems to prioritize select components to maintain safety, instead of focusing on all components.
We examine charging stations for electric vehicles as a case study on graceful degradation and trust boundries. EV charging station have a large, modular architecture with a minimal interaction between local stations. Identifying the trust boundry for this system can show that graceful degradtion is applicable to real world systems and provides details of improvement regions to fulfillment of safety-critical requirements.
Secure multiparty computation (MPC) is a cryptographic process that allows for mathematical computation over masked and unknown inputs. MPC deployments are used in a variety of areas, including medical and economic research, as well as cryptocurrencies and digital key wallets. However, many MPC implementation (including those implemented by MPC cryptographers) have security gaps and bugs. Even when implementations are theoretically secure, they can still be crippled by the domain they are deployed in - the context of the deployment as well the hardware infrastructure the computation runs on. While there has been much work in proving theoretical MPC protocols, as well as formal models for MPC compillers, there is little work in formally verifying MPC. In this work, we create formal models of different MPC protocols, and include the hardware infrastructure context within the model to identify security vulnerabilities. This allows for identification of security vulnerabilities that exist due to hardware configurations that cannot be reasoned about during cryptographic proofs.