安全是所有企业的重中之重。无论是改善安全状况，实施全面合规控制，还是让员工安全地在家办公，企业都需要有可靠的系统作为支撑。但是，随着企业系统规模的空前壮大，合规要求也日益变得更复杂，企业需要新的解决方案。

在基础设施安全方面，企业希望有确凿的证据和方法来确定其访问管理、网络基础设施和应用程序的安全能够无懈可击。云计算通过联网方式为企业按需提供 IT 资源，其好处之一就是使企业能够利用原来无法在本地获得的现代化技术来更有信心地保护其基础设施的安全。

其中一种现代化的方法就是可证明的安全性，它通过数学证明来验证系统是否正确运行。对拥有成千上万资源的大型企业，如果通过手动评估不同场景中的每一项数据路径及相关的控制，来证明系统运行的正确性和安全性，通常需要花费数月乃至数年的时间。而且在这个评估期间，系统本身还在不断变化和演进。借助自动化推理这一新兴技术，这样的工作可以在数秒内完成。

通过可证明安全性实现规模化安全

自动化推理是可证明安全性的核心。通过考虑各种可能的应用执行、请求和配置，自动化推理可以提前预判出系统的可能操作，并提供高级别的安全保证。例如，自动化推理工具可以分析策略和网络配置，证明没有潜在的安全威胁。客户采用这种前沿技术，可以不断地自动化、简化云上安全路径，持续解决软件系统演变过程中可能出现的意外风险。

亚马逊云科技运行着数以十万计的客户关键任务工作负载，将该技术广泛应用于存储、网络、虚拟化和加密等关键领域来提升安全性，也是首家规模化使用自动化推理的云服务提供商。客户广泛使用的诸多重点服务如身份与访问管理服务​​Amazon Identity and Access Management (IAM)​​​，对象存储服务​​Amazon Simple Storage Service (S3)​​​，​​Amazon Virtual Public Cloud (VPC)​​等都用到了这一技术。这一技术的应用使得政府机构、医疗和金融服务等被高度监管的行业客户，正在用与过去完全不同的方式在云上更安全的运行业务。

亚马逊云科技开发了多种自动化推理工具帮助客户实现应用的可证明安全性。其中一个工具可以大规模地分析访问控制策略，为 ​​Amazon IAM Access Analyzer​​​、​​Amazon S3 Block Public Access​​​等服务提供功能支持。这些功能确保 “不受限制的公开访问”的不被授权，使客户能够迅速识别对其云资源的越权访问，并加以补救。另一个工具可以在几秒之内检查所有网络路径，并为​​Amazon VPC Reachability Analyzer​​​以及 ​​Amazon Inspector​​等服务提供支持，帮助客户了解其使用的亚马逊云科技网络的安全与合规，并采取行动加以改善。

携手共同实现安全性

客户不需要成为安全专家或是数学家就能实现其软件的完整性，并管理其关键基础设施。事实上，作为一名科学家，我之所以研究、设计、构建和实施可证明安全性工具来确保持续的云安全，就是为了让企业可以将更多精力放在业务扩展和转型上。

借助亚马逊云科技，企业无需管理繁重的底层工作以及预付费用，就可以借助如机器学习、物联网、数据湖、数据分析等复杂技术完成企业的重要任务。这样客户就可以做真正重要的事情——快速、灵活和大规模地进行业务创新。

让自动化成为标准

可证明安全性还处于早期发展阶段。尽管自动化推理只在最近才得以实际应用，亚马逊云科技正在努力使此项技术变为日常工程标准，来为客户创造功能更为强大的、易用的工具。