首页 文章 精选 留言 我的
优秀的个人博客,低调大师

微信关注我们

原文链接:https://www.oschina.net/news/216876

转载内容版权归作者及来源网站所有!

低调大师中文资讯倾力打造互联网数据资讯、行业资源、电子商务、移动互联网、网络营销平台。持续更新报道IT业界、互联网、市场资讯、驱动更新,是最及时权威的产业资讯及硬件资讯报道平台。

NVIDIA 尝试使用 SPARK 语言取代部分 C 语言代码

知名编程语言 Ada 与 SPARK 所属公司 AdaCore 发布了一则关于NVIDIA 的案例 ,案例显示:NVIDIA 的产品运行着许多经过正式验证的 SPARK 代码,NVIDIA 安全团队正尝试使用 SPARK 语言取代 C 语言,来实现一些对安全较为敏感的应用程序或组件。 SPARK 是一种编程语言和一组验证工具,旨在满足高保证软件开发的需求。SPARK 基于 Ada 语言,它既对 ada 语言进行子集化以删除无法验证的功能,又扩展了合约和方面的系统,进一步支持模块化、形式化验证。 SPARK 语言一般用于可预测和高度可靠操作的系统中的高完整性软件,它有助于开发需要高安全性或业务完整性的应用程序。 早在 2018 年, NVIDIA 就针对“从 C 转换为 SPARK”这一过程进行了概念验证 (POC) 练习,在三个月内将两个低级别的安全敏感应用从 C 转换为 SPARK 代码。在对投资回报进行评估后,该团队得出结论:随着新技术的增加(培训、实验、新工具等),应用程序安全性和验证效率也得到了提高,转换为 SPARK 代码的两个应用程序实现了安全稳健性的重大改进(有关评估结果...

OpenHarmony移植案例: build lite源码分析之hb命令__entry__.py

摘要:本文介绍了build lite 轻量级编译构建系统hb命令的源码,主要分析了_\entry__.py文件。 本文分享自华为云社区《移植案例与原理 - build lite源码分析 之 hb命令__entry__.py》,作者:zhushy 。 hb命令可以通过python pip包管理器进行安装,应该是OpenHarmony Build的缩写,在python包名称是ohos-build。hb作为编译构建子系统提供的命令行,用于编译构建产品、芯片厂商组件或者单个组件。我们来学习hb命令行工具的源码,本文主要分析下文件openharmony/build/lite/hb/__entry__.py。 1、find_top()函数 find_top()函数用于获取OpenHarmony源代码根目录,之前的系列文章分析过。代码也较简单,不再赘述。 def find_top(): cur_dir = os.getcwd() while cur_dir != "/": hb_internal = os.path.join(cur_dir, 'build/lite/hb_internal')...

相关文章

发表评论

资源下载

更多资源
优质分享App

优质分享App

近一个月的开发和优化,本站点的第一个app全新上线。该app采用极致压缩,本体才4.36MB。系统里面做了大量数据访问、缓存优化。方便用户在手机上查看文章。后续会推出HarmonyOS的适配版本。

Mario

Mario

马里奥是站在游戏界顶峰的超人气多面角色。马里奥靠吃蘑菇成长,特征是大鼻子、头戴帽子、身穿背带裤,还留着胡子。与他的双胞胎兄弟路易基一起,长年担任任天堂的招牌角色。

Nacos

Nacos

Nacos /nɑ:kəʊs/ 是 Dynamic Naming and Configuration Service 的首字母简称,一个易于构建 AI Agent 应用的动态服务发现、配置管理和AI智能体管理平台。Nacos 致力于帮助您发现、配置和管理微服务及AI智能体应用。Nacos 提供了一组简单易用的特性集,帮助您快速实现动态服务发现、服务配置、服务元数据、流量管理。Nacos 帮助您更敏捷和容易地构建、交付和管理微服务平台。

Spring

Spring

Spring框架(Spring Framework)是由Rod Johnson于2002年提出的开源Java企业级应用框架,旨在通过使用JavaBean替代传统EJB实现方式降低企业级编程开发的复杂性。该框架基于简单性、可测试性和松耦合性设计理念,提供核心容器、应用上下文、数据访问集成等模块,支持整合Hibernate、Struts等第三方框架,其适用范围不仅限于服务器端开发,绝大多数Java应用均可从中受益。