Local-first software manages and processes private data locally while still enabling collaboration between multiple parties connected via partially unreliable networks. Such software typically involves interactions with users and the execution environment (the outside world). The unpredictability of such interactions paired with their decentralized nature make reasoning about the correctness of local-first software a challenging endeavor. Yet, existing solutions to develop local-first software do not provide support for automated safety guarantees and instead expect developers to reason about concurrent interactions in an environment with unreliable network conditions. We propose LoRe, a programming model and compiler that automatically verifies developer-supplied safety properties for local-first applications. LoRe combines the declarative data flow of reactive programming with static analysis and verification techniques to precisely determine concurrent interactions that violate safety invariants and to selectively employ strong consistency through coordination where required. We propose a formalized proof principle and demonstrate how to automate the process in a prototype implementation that outputs verified executable code. Our evaluation shows that LoRe simplifies the development of safe local-first software when compared to state-of-the-art approaches and that verification times are acceptable.


翻译:基于本地优先的软件可以在本地管理和处理私有数据,同时仍然允许通过部分不可靠的网络连接的多个参与方之间的协作。这样的软件通常涉及与用户的交互和执行环境(外部世界)的交互。这些交互的不可预测性以及它们的分散性使得推断基于本地优先的软件的正确性成为一项具有挑战性的努力。然而,现有的解决方案开发基于本地优先的软件不提供支持自动化安全性保证,而是期望开发人员在具有不可靠网络条件的环境中推断并发交互。我们提出了LoRe,这是一种编程模型和编译器,用于自动验证基于本地的应用程序的开发人员提供的安全属性。LoRe将响应式编程的声明性数据流与静态分析和验证技术相结合,以准确确定违反安全不变量的并发交互,并有选择地通过协调采用强一致性。我们提出了一个形式化的证明原则,并演示了如何在原型实现中自动化该过程输出已验证的可执行代码。我们的评估显示,与现有的最新方法相比,LoRe简化了开发安全的基于本地优先的软件的过程,并且验证时间是可接受的。

1
下载
关闭预览

相关内容

抢鲜看!13篇CVPR2020论文链接/开源代码/解读
专知会员服务
49+阅读 · 2020年2月26日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
机器学习相关资源(框架、库、软件)大列表
专知会员服务
39+阅读 · 2019年10月9日
云开发的崛起和localhost的终结
InfoQ
0+阅读 · 2022年11月11日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
时序数据异常检测工具/数据集大列表
极市平台
65+阅读 · 2019年2月23日
LibRec 精选:推荐系统的常用数据集
LibRec智能推荐
17+阅读 · 2019年2月15日
LibRec 精选:推荐系统的论文与源码
LibRec智能推荐
14+阅读 · 2018年11月29日
LibRec 精选:基于LSTM的序列推荐实现(PyTorch)
LibRec智能推荐
50+阅读 · 2018年8月27日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
1+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2023年6月1日
Arxiv
0+阅读 · 2023年5月31日
Arxiv
20+阅读 · 2019年11月23日
VIP会员
相关VIP内容
抢鲜看!13篇CVPR2020论文链接/开源代码/解读
专知会员服务
49+阅读 · 2020年2月26日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
机器学习相关资源(框架、库、软件)大列表
专知会员服务
39+阅读 · 2019年10月9日
相关基金
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2011年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
国家自然科学基金
1+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员