- Scy-tsg - lists.openatom.io

[RFC] Inclusion of Libvsync and Asap tool in openHarmony

by Diogo Behrens

Dear mailing list, we would like to include a library and a verification tool in the openHarmony family. This work is the result of more than 3 years of research by the concurrency team in the Huawei Dresden Research Center. In the following, I'll describe how this inclusion could improve the safety and security of the openHarmony ecosystem. # Context: Concurrency in system software We know that exploiting the hardware parallelism provided by multicore CPUs is a necessary step to achieve performance and competitiveness. Most software is nowadays multithreaded. That includes the kernel, services, databases, and the applications. Concurrent programs are, however, very tricky to get right. The costs of debugging and performing postmortem analysis is huge in due to the non-deterministic nature of concurrent executions. In every program execution, threads interleave in different ways not only producing (potentially) different outcomes, but also exercising different thread interactions via shared memory accesses. Within these interactions, subtle bugs reside, waiting to be triggered. They may cause a variety of undesirable effects such as crashes, data corruption, and hangs. The cost of concurrency bugs is specially critical in the kernel and system libraries, which are the basis for the rest of the ecosystem. In contrast to sequential code, there is no well-established approach to test concurrent code at the moment. Often such code is barely tested. Existing techniques such as formal verification, model checking, and systematic testing require expertise and seldom belong to the developer's toolbelt. # Proposal: a verified synchronization library and a verification tool We propose to tackle concurrency challenges in system software with practical verification: a path explored for 3 years in the Huawei Dresden Research Center, and recognized within Huawei and by the academic community (eg, see [1,2,3,4]). To let the developers focus on the software functionality and at the same time to guarantee correctness of the concurrent portions of the source code, we suggest the use of two complementary approaches: 1. A battle-proof, extensively tested, and formally verified library of data structures and synchronizations primitives. 2. Practical tools to support the development of custom concurrent data structures matching the user's needs. ## Libvsync: verified synchronization primitives and data structures Our libvsync is such a verified library. Libvsync contains low-level atomics, synchronization primitives, and several common concurrent data structures that can be safely used in C/C++ programs on x86, Arm or RISC-V processors. Our library has been extensively tested and substantial portions have been verified with model checkers (see tools below). In particular, Libvsync has been verified to work on architectures with Weak Consistency Memory Models such as ARMv7, ARMv8, and RISC-V. Within Huawei, Libvsync has been extensively deployed, helping products (including the HongMeng kernel) to better use the available hardware parallelism and achieve a higher confidence of correctness. ## ASAP: As Safe As Possible Accompanying the library, we have developed a set of tools to test and verify it. We would like to opensource Asap: Asap takes a test case of a concurrent code and, using the opensource model checkers GenMC[7] and Dartagnan[8], verifies whether the code is safe and live. Asap takes into account the memory model of the target architecture, which is configurable and can represent x86, ARMv8, Linux Kernel memory model, among others. Moreover, to improve synchronization performance, asap optimizes use of memory barriers (relaxing them), while guaranteeing the concurrent code is still correct. A set of elaborated techniques allow Asap to perform the search for a maximally-relaxed combination of barriers and fences in a very short time. Libvsync's CI/CD pipeline runs asap on every code merged into the library. But Asap is not limited to code inside Libvsync. It has been also used to verify code from the Linux Kernel[5] and components in other Huawei operating systems. With Asap we were also able to find bugs in existing opensource projects such as DPDK buf_ring[9] and CLH lock in seL4 microkernel[10]. # Benefits of open sourcing Libvsync and Asap Libvsync and Asap form a strong solution to support development of high-performant, safe, and scalable system software. They are already well recognized within Huawei and by the academia and resulted in several publications. We believe that Libvsync and Asap can enhance the openHarmony ecosystem. Libvsync provides the user with off-the-shelf verified, scalable code. Asap supports the implementation of advanced data structures that safe and live. As far as we are aware, no other platforms/community includes equally powerful solutions in their standard ecosystems. Furthermore, given the large numbers of requests from the academic community for access to these projects, we think that opening them can raise the awareness of top-tier researchers to the openHarmony project. # Request We kindly ask for your feedback. Would the community be interested in including Libvsync and Asap as two new projects? If yes, what would be the process to follow? Thank you. Best regards, -Diogo # References - [1] VSync: verification and optimization for synchronization primitives on weak memory models (Best paper at ASPLOS'20) https://dl.acm.org/doi/10.1145/3445814.3446748 - [2] Verifying and Optimizing the HMCS Lock for Arm Servers https://link.springer.com/chapter/10.1007/978-3-030-91014-3_17 - [3] CLoF: Compositional Lock Framework for Multi-level NUMA Systems SOSP'21 -- https://dl.acm.org/doi/10.1145/3477132.3483557 - [4] BBQ: Block-based Bounded Queue -- USENIX ATC'22 https://www.usenix.org/conference/atc22/presentation/wang-jiawei - [5] Verifying and Optimizing Compact NUMA-Aware Locks on WMMs https://arxiv.org/abs/2111.15240 - [7] GenMC: https://github.com/MPI-SWS/genmc - [8] Dartagnan: https://github.com/hernanponcedeleon/Dat3M - [9] DPDK bug_ring bug: http://patches.dpdk.org/patch/75983/ - [10] seL4 bug: https://github.com/seL4/seL4/pull/199

1 year, 3 months

3
2
0 0

OH难题模板

by 张春辉

各位安全与机密计算TSG成员，大家好： OH将于11月份举行技术峰会，峰会上会发布十大难题，机密计算TSG可通过回应难题，在大会上提升本TSG技术影响力。现将难题模板发给大家。难题需要发送到：tsc(a)openharmony.io 感谢大家。

1 year, 5 months

4
6
0 0

【会议通知】 OpenHarmony安全及机密计算TSG例会，时间：2022-10-26 14:10-15:10(UTC+08:00)Beijing

by Meeting Book

会议主题 Subject OpenHarmony安全及机密计算TSG例会会议时间 Time 2022-10-26 14:10-15:10 (UTC+08:00)Beijing 会议地点 Location Welink视频会议 Welink Video Meeting 加入会议(External)<https://meeting.huaweicloud.com:36443/#/j/98763309> 会议ID Meeting ID 98763309 召集人 Convener 陆成刚提示 Tips 请点击会议链接加入会议,首次使用请在入会界面根据提示下载并安装客户端后输入ID入会。 Click the meeting link to join the meeting. For the first time, download and install the client as prompted and enter the ID to join the meeting

1 year, 6 months

1
0
0 0

OH技术直播平台筹备，欢迎TSG各位老师报名授课布道！！//转发: 【请您知悉】计划启动OpenHarmony Tech Club系列直播课，请TSC成员单位、各TSG协助参与直播课筹备，谢谢~

by Luchenggang

主题: 【请您知悉】计划启动OpenHarmony Tech Club系列直播课，请TSC成员单位、各TSG协助参与直播课筹备，谢谢~ 各位TSC成员和 TSG负责人：大家好！ l 背景：为持续构建OpenHarmony开源项目以及TSC、TSG的社会影响力，打造前沿性、有深度、成体系的样版品牌直播课程，“OpenHarmony Tech Club系列直播课”现已完成初步活动策划，拟于11月启动。预计每两周或三周进行一期课程直播，每一期会邀请一位嘉宾老师进行技术直播课程分享。初步策划如下，详情见附件PPT： [cid:image001.png@01D8E79D.A7196250] l 诉求为输出高质量的系列直播课内容，我们初步设想，希望由TSC成员单位、各TSG作为主要的内容提供方，大家轮流贡献技术主题并进行直播分享，课程内容框架详细设计和排班计划还在进一步细化中。为减少对TSC成员和TSG负责人的打扰，我们会与大家前期提供的接口人进行对接。请各位接口人，于11月4日/星期五下班前，按照如下模板反馈直播主题至廖涛liaotao11(a)huawei.com<mailto:liaotao11@huawei.com>，非常感谢~ 主题名称涉及领域分享日期（暂时仅收集11月、12月主题） 11月/12月（二选一） l 附：接口人信息汇总 TSC成员接口人姓名陈海波张沫武延军朱伟臧斌宇杜东张兆生姚全丽张荣超石磊李英伟张诗悦贾宁张春辉 TSG名称接口人姓名编程语言TSG 王学智跨平台框架TSG 陈功平安全及机密计算TSG 陆成刚 Web3标准TSG Wenjing Chu 如有任何建议或者疑问，可通过以下联系方式随时联系廖涛。廖涛 OH TSC运营支撑组 Mobile：+86 15804031261 Email: liaotao11(a)huawei.com<mailto:liaotao11@huawei.com>

1 year, 6 months

1
0
0 0

安全及机密计算TSG白皮书写作分工

by Luchenggang

各位老师好，关于安全及机密计算TSG白皮书写作分工，还请大家发表意见，看是否合适哈，多谢如无问题，我们每一章节再确定一位写作牵头人，采用腾讯文档开始在线写作。 1、数字经济驱动数据成为市场经济的核心生产要素 --- 李风华/郭云川/吴少铎 ( 隐私保护技术对数据经济发展的价值意义) 1.1数字经济发展不断迈向新高度 1.2数据成为数字经济核心生产要素 1.3数据安全流通是发展数字经济的关键 2、数据交易与数据市场当前面临的安全隐私挑战 --- 贾良玉/杨坤/闫博文 2.1 数据违规采集流动及泄露风险加剧 2.2 数据交易流通面临技术挑战 2.3 隐私计算技术规模化应用挑战 3、数据安全及密码学技术发展趋势洞察 ---何道敬/李大为/潘适然 4、隐私计算与机密计算技术概览 --- 夏虞斌/杜东/陆成刚/张春辉 4.1 隐私计算技术体系的发展态势 4.2 机密计算技术概览 ARM（Trustzone/CCA）、Intel（SGX/TDX）、AMD（SEV）、RISC-V（keystore/蓬莱enclave）等 5、异构机密计算 --- 金意儿/华佳锋 6、OpenHarmony安全与机密计算技术发展总结 --- 付天福/陆成刚/潘适然/张春辉

1 year, 6 months

1
0
0 0

烦请各位TSG成员审核纪要//【会议纪要】OpenHarmony技术指导委员会安全及机密计算TSG会议纪要（20220928）

by Luchenggang

TSG��Ҫ��鵵��Gitee��λTSG��Ա��˼�Ҫ��лл��~ ======================= OpenHarmony��ָ��ίԱ�ᰲȫ��ܼ��TSG��Ҫ��20220928�� ʱ �� 2022��9��28�� 15:30-16:30 �ص� ��ϻ�� TSG��Ա ��츣��Ϊ��٣��ﻪ��ί�У��Ʋ��ġ��ε��졢½�ɸա��ί�У��ݱ󡢼��Ȼ ��ϱʻ�� Ա ��Ϊ ȱϯ��Ա ��ϯ��Ա / �� 1��⼰TSG��Ϣͬ��TSG��⼰TSG��Ƥ��չ ��2��DLP��ݷ�й©��Ŀ�� λ��Ҫ��: һ�� ⼰TSG��Ϣͬ��TSG��⼰TSG��Ƥ��չ��㱨��: ½�ɸգ� 1 ��TSG��Ա��ȫ��ս��⵽tsc@openharmony.io��᰸��TSG�ʼ��б��ۡ��ύ��ֹʱ��10.30 2 TSG��Ƥ��ʼ��б��һ��ۣ��TSG��Ա��첢�ֹ�д�� DLP��ݷ�й©��Ŀ��󣨻㱨��: ��Ȼ�� 1��OpenHarmony��ݷ�й©��ǰ��ע��ܿط��Ա�΢��RMS�� 2��ǰ��Կ��֤�ͷ��ʿ��Ʋ��Եİ�ȫ�ԣ��Լ��̬�Ѻ��湹��Ŀ��ϵͳ��ݷ��ʿ��Ʋ��ԵĹܿأ� 3��漰��֤��Կ��ȶ��Ĺؼ��ϸ��Ҫ��ϸ��ۣ� 4��ڿ�Դ��ԣ��ص㶨�尲ȫ�ܹ��Э��׼��幦��ɸ��ʵ�֡� ��ʮ�� : Luchenggang ��ʱ��: 2022��9��9�� 17:45 �ռ��: Futianfu (FU Tianfu, CBG) <futianfu(a)huawei.com>; jinyier <yier.jin(a)huawei.com>; panshiran <panshiran(a)huawei.com>; 'hedaojinghit(a)163.com' <hedaojinghit(a)163.com>; 'jialy(a)hotmail.com' <jialy(a)hotmail.com>; 'lifenghua(a)iie.ac.cn' <lifenghua(a)iie.ac.cn>; 'li.dawei(a)hit.edu.cn' <li.dawei(a)hit.edu.cn>; 'wushaoduo(a)kaihong.com' <wushaoduo(a)kaihong.com>; 'xiayubin(a)sjtu.edu.cn' <xiayubin(a)sjtu.edu.cn>; 'yanbowen(a)uniontech.com' <yanbowen(a)uniontech.com>; 'yiqundayan(a)outlook.com' <yiqundayan(a)outlook.com>; 'luchgang(a)gmail.com' <luchgang(a)gmail.com> ��: Jianing (OS-LAB) <ning.jia(a)huawei.com>; Liuguo (A) <macin.liu(a)huawei.com> ��: ��λTSG��Ա��˼�Ҫ//��Ҫ��OpenHarmony��ָ��ίԱ�ᰲȫ��ܼ��TSG��Ҫ��20220909�� TSG��Ҫ��鵵��Gitee��λTSG��Ա��˼�Ҫ��лл��~ ϣ��9��15��°�ǰ�յ��Ĵ𸴣�лл~ ======================= OpenHarmony��ָ��ίԱ�ᰲȫ��ܼ��TSG��Ҫ��20220909�� ʱ �� 2022��9��9�� 14:15-15:30 �ص� ��ϻ�� TSG��Ա ��츣��Ϊ��ﻪ��ȱϯ��Ʋ��(ί��)��ε��졢½�ɸա��٣��ݱ󡢼��ί�У��Ȼ ��ϱʻ�� Ա �� ȱϯ��Ա ��ﻪ ��ϯ��Ա / �� 1��⼰TSG��Ϣͬ�� 2��Ƥ��д�� 3��enclave��Ŀ�� 4��뿪Դ��Ŀ��ۣ�Ŀ�꽨��Ȩ��㷨��Դ�� λ��Ҫ��: һ�� ⼰TSG��Ϣͬ��㱨��: ½�ɸգ� TSC��TSC��ں��ݷ��ƽ̨��TSG��Ա��Ϣ��TSG�ʼ��б��TSG��Ŀ��Ȩ��Ʒ�ƾ�� 1 ȷ�Ͽ�Դ��Ŀ��Ӫ��֯��Ȩ��⣬��Ŀ��𷽿��ƻ��TSG��ƣ�maintainer/committer�� -- ½�ɸ� 2 ȷ�ϼ��ս��᰸ʱ�䣬��TSG��ڵ� -- ½�ɸ� 3 �ʼ��б��شٸ�TSG��Ա��ע�� -- ½�ɸ� ��ȫ��ܼ��TSG��Ƥ��д��ۣ��㱨��: ½�ɸգ� 1 ��֯��Ƥ��д��ٵ��ݷֽ�� -- ½�ɸ� 2 ��Ƥ��д��ͳһ��Э��д��ƽ̨�� -- ½�ɸ� ��enclave��Ŀ�� 㱨��: ��ݱ� ��ۣ�GO 1��OpenHarmony��ͳһ�Ķ��TA��API��̽ӿڣ��̬��ݣ�ͳһ�Ľӿڱ�׼��Ժ�OH��TEE SIG�Խӣ� 2��ɶԽ�֧�ֺ�˼��RISC-VоƬ��Ϊ��case�� 3��֧��RISC-V��Cortex-M��MIPS�ȿ�оƬ�ܹ��Ŀ�ܣ��Ŀ��̬�� 4��ǶԽӰ�ȫоƬSIG��ͳһ�ӿڣ�֧�ְ�ȫоƬ�Ľ��루��ȫоƬSIG�ڷ��Դ��ȫоƬ�Ĺ��ܼ��ӿڱ�׼�� 5��Ŀ�ƻ�� ġ��뿪Դ��Ŀ��ۣ�Ŀ�꽨��Ȩ��㷨��Դ�⣨�㱨��: ��Ϊ��ε�� 1��OpenSSL��mbedTLS��׼��迪��䣻 2��ǰ�͹��Ժ�ȵ�λ�Խӣ��ȡ��Ŀ��ʱ��ɻ�ù��֤�� 3��Խ��л��ʵ��ҡ��Ź��Ϻ��ѧ��ʦ��ʦ��ר��һ�� -- ��Ȼ ��: �� ƻ��ر�ʱ�� 1 ȷ�Ͽ�Դ��Ŀ��Ӫ��֯��Ȩ��⣨maintainer/committer�� ½�ɸ� 2022��9��25�� 2 �شٴ��ʼ��б�ע�ᣬ��չTSG��Ƥ�顢��ۣ�ȷ�ϰ�Ƥ��д��ƽ̨ ½�ɸ� 2022��9��25�� 3 ��л��ʵ��ҡ��Ź��Ϻ��ѧ��ʦ��ʦ��ר�Ҳ��뿪Դ��Ŀ ��Ȼ 2022��9��25�� ¾�� : Luchenggang ��ʱ��: 2022��8��24�� 18:37 �ռ��: Futianfu (FU Tianfu, CBG) <futianfu(a)huawei.com<mailto:futianfu@huawei.com>>; jinyier <yier.jin(a)huawei.com<mailto:yier.jin@huawei.com>>; panshiran <panshiran(a)huawei.com<mailto:panshiran@huawei.com>>; 'hedaojinghit(a)163.com' <hedaojinghit(a)163.com<mailto:hedaojinghit@163.com>>; 'jialy(a)hotmail.com' <jialy(a)hotmail.com<mailto:jialy@hotmail.com>>; 'lifenghua(a)iie.ac.cn' <lifenghua(a)iie.ac.cn<mailto:lifenghua@iie.ac.cn>>; 'li.dawei(a)hit.edu.cn' <li.dawei(a)hit.edu.cn<mailto:li.dawei@hit.edu.cn>>; 'wushaoduo(a)kaihong.com' <wushaoduo(a)kaihong.com<mailto:wushaoduo@kaihong.com>>; 'xiayubin(a)sjtu.edu.cn' <xiayubin(a)sjtu.edu.cn<mailto:xiayubin@sjtu.edu.cn>>; 'yanbowen(a)uniontech.com' <yanbowen(a)uniontech.com<mailto:yanbowen@uniontech.com>>; 'yiqundayan(a)outlook.com' <yiqundayan(a)outlook.com<mailto:yiqundayan@outlook.com>> ��: Jianing (OS-LAB) <ning.jia(a)huawei.com<mailto:ning.jia@huawei.com>>; Liuguo (A) <macin.liu(a)huawei.com<mailto:macin.liu@huawei.com>> ��: ��λTSG��Ա��˼�Ҫ//��Ҫ��OpenHarmony��ָ��ίԱ�ᰲȫ��ܼ��TSG��Ҫ��20220823�� TSG��Ҫ��鵵��Gitee��λTSG��Ա��˼�Ҫ��лл��~ ϣ��8��25��°�ǰ�յ��Ĵ𸴣�лл~ ======================= OpenHarmony��ָ��ίԱ�ᰲȫ��ܼ��TSG��Ҫ��20220823�� ʱ �� 2022��8��23�� 14:15-15:30 �ص� ��ϻ�� TSG��Ա ��츣��Ϊ��ﻪ��Ʋ��ġ��ε��졢½�ɸա��ݱ󡢼��Ȼ ��ϱʻ�� Ա / ȱϯ��Ա / ��ϯ��Ա ��TSG��ʦ��TSC��Ӫ�� 1��OH��ȫ��ܼ��TSG��Ա��ҽ�� 2��OH��ȫ��ܼ��TSGԸ��Ŀ�꼰ְ�� 3��ȫ��ܼ��TSG��ʽ��ڹ��ƻ�� һ��λ��Ҫ��: ��1��OH��ȫ��ܼ��TSG��Ա��ҽ�� Ҫ: �� 2��OH��ȫ��ܼ��TSGԸ��Ŀ�꼰ְ�𣨻㱨��: ��츣�� Ҫ: 1��ܰ�ȫ��ܼ��TSG��Ŀ�귶Χ��̽��Ŀʾ�� 2��ȫ��ܼ��TSG��Ŀ��Χ��OpenHarmony��Խ��п�OS��ȫ��̬��̽��ݰ�ȫ��ϵͳ��ȫ ��3��ȫ��ܼ��TSG��ʽ��ڹ��ƻ��ۣ��㱨��: ½�ɸ� �� Ҫ: 1��Ļ��ڣ�ǰ�ڽ��2��һ�Σ�9��Ѯ��չ��һ�� 2��³�Ա��룬��Ȳ��TSG��Ŀ��ݹ��׼��ͶƱ�� 3��TSG��Ŀ֪ʶ��Ȩ��⡢��ĿЭ��ǩ��Ŀ��ɡ��ҵ��׼�� 4��TSG��Ŀ��û�б�׼ģ�壬�ɲο�PMC��SIG��Ŀ��ģ�� 5��ڰ�ȫ��ܼ��Ƥ�飬��٣��ֹ�д�� : �� ƻ��ر�ʱ�� 1 ��֯TSG��Ա�ṩ��Ƭԭͼ��Ƹ��˼�� ½�ɸ� 2022��9��5�� 2 TSG��Ŀ��ı�׼��ͳһ��TSG��λ��Ա �� 2022��9��5�� ¶�ʮ��

1 year, 6 months

2
2
0 0

TSG成员gitee账号，如有误请反馈

by Luchenggang

TSG成员：付天福：@futianfu 李凤华：@lifenghua 李大为：@ldwhit 何道敬：@he-daojing 夏虞斌：@xiayubin 贾良玉：@asimovky 金意儿：@jinyier 吴少铎：@wu-shao-99 闫博文：@jouyouyun 陆成刚：@itrustee 潘适然：@shiran_pan

1 year, 6 months

1
0
0 0

TSG成员gitee账号，请大家确认

by Luchenggang

TSG成员：付天福：@futianfu 李凤华：@lifenghua 李大为：@ldwhit 何道敬：@he-daojing 夏虞斌：@xiayubin 贾良玉：@asimovky 金意儿：@jinyier 吴少铎：@wu-shao-99 闫博文：@yanbowen 陆成刚： @iTrustee 潘适然：@shiran_pan

1 year, 6 months

1
0
0 0

请TSG成员按邮件中说明，反馈下gitee账号吧//答复: 【请您协助】烦请各位TSG负责人收集并反馈TSG成员的gitee账号，谢谢~

by Luchenggang

TSG成员：付天福：李凤华：@lifenghua 李大为：何道敬：夏虞斌：@xiayubin 贾良玉：金意儿：@jinyier 吴少铎：闫博文：@yanbowen 陆成刚： @iTrustee 潘适然：发件人: Maojingmin 发送时间: 2022年9月28日 14:47 收件人: Wangxuezhi (A) <tony.wangxuezhi(a)huawei.com>; yuzhiqiang (E) <yuzhiqiang5(a)huawei.com>; Futianfu (FU Tianfu, CBG) <futianfu(a)huawei.com>; Luchenggang <luchenggang(a)huawei.com>; w00389623 <wchu(a)futurewei.com> 抄送: Liuguo (A) <macin.liu(a)huawei.com> 主题: 【请您协助】烦请各位TSG负责人收集并反馈TSG成员的gitee账号，谢谢~ 以TSG位单位，希望9月30日/周五下班前能收到各TSG所有成员的Gitee账号，给您添麻烦了，非常感谢~ 【Gitee账号申请说明】 1、Gitee账号注册链接为：https://gitee.com/help/articles/4113 2、注册成功后，请您点击网站右上角的“个人主页”，复制Gitee账号即可。（注意：gitee账号格式为@XXXX，您只需要提供@及之后的字符串，见以下示意图的红框内字段。!!!为避免返工，一定要看清楚哦） [cid:image003.png@01D8DB01.A8983FF0] 【其他建议】为方便各TSG快速收集信息，在此提供一些的小tips，供您参考： 1、方式一：微信群接龙 2、方式二：微信小程序“腾讯问卷”、或者“腾讯文档”的“在线表格”功能

1 year, 6 months

1
0
0 0

Re: test for subscribe mail list

by Yubin Xia

(空邮件-2)

1 year, 6 months

1
0
0 0

2024

2023

2022

Scy-tsg