Formal methods are increasingly adopted in systems where reliability and correctness are critical, enabled by improvements in tool usability, speed, and automation. This industrial experience report presents three projects at Huawei Cloud showcasing different trade-offs in investment and assurance levels. We applied probabilistic concurrency testing, model checking, and deductive verification to two foundational services in the database and networking domains: the K2 transactional key-value store and the Global Server Load Balancer (GSLB).

The ability to exchange data while maintaining sovereignty is fundamental to emerging decentralized data-driven ecosystems. Data sovereignty refers to the entity's capability to be self-determined concerning data usage. As such, a data usage control system (UCON) is critical for sovereignty. UCON, a generalization of attribute-based access control, enforces continuous authorization, allowing attribute mutability after access is granted. In theory, UCON comprises a policy language to express constraints and obligations of data usage, and a technology to evaluate and enforce them. In practice, realizing the above is challenging and poses trust concerns. Partly, this is due to the complexity of UCON (continuous authorization, obligations) and the advanced usage constraints (stemming from, e.g., regulations or business contracts) combined with the decentralized nature of data ecosystems that allow different actors (e.g., data provider, security engineers) to author policies, and operate UCON. To that end, we propose to aid actors with automated policy analysis and verification methods. We present a new policy analysis method based on the combination of symbolic execution for policy evaluation and SMT solving to compute concrete scenarios answering queries on the policies. Our approach supports symbolic queries, where attribute values may be concrete values, a range of values, or symbolic variables. We also propose a monitoring approach using RTLola tool to verify the correctness of UCON's behavior in terms of decisions, obligations, and user-specified properties. To monitor obligations, we define their essential parameters and show how to monitor their fulfillment based on the configuration. We also present eight templates that allow users to generate the most important properties for monitoring UCON.