Document Open Access Logo

DeFiAligner: Leveraging Symbolic Analysis and Large Language Models for Inconsistency Detection in Decentralized Finance

Authors Rundong Gan, Liyi Zhou, Le Wang , Kaihua Qin, Xiaodong Lin

PDF
Thumbnail PDF

File

LIPIcs.AFT.2024.7.pdf
  • Filesize: 2.17 MB
  • 24 pages

Document Identifiers

Author Details

Rundong Gan
  • School of Computer Science, University of Guelph, Canada
Liyi Zhou
  • The University of Sydney, Australia
  • UC Berkeley RDI, CA, USA
  • Decentralized Intelligence AG, Zug, Switzerland
Le Wang
  • School of Computer Science, University of Guelph, Canada
Kaihua Qin
  • Yale University, New Haven, CT, USA
  • UC Berkeley RDI, CA, USA
  • Decentralized Intelligence AG, Zug, Switzerland
Xiaodong Lin
  • School of Computer Science, University of Guelph, Canada

Funding

This work was supported in part by the Natural Sciences and Engineering Research Council of Canada (NSERC).

Cite As Get BibTex

Rundong Gan, Liyi Zhou, Le Wang, Kaihua Qin, and Xiaodong Lin. DeFiAligner: Leveraging Symbolic Analysis and Large Language Models for Inconsistency Detection in Decentralized Finance. In 6th Conference on Advances in Financial Technologies (AFT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 316, pp. 7:1-7:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.AFT.2024.7

Abstract

Decentralized Finance (DeFi) has witnessed a monumental surge, reaching 53.039 billion USD in total value locked. As this sector continues to expand, ensuring the reliability of DeFi smart contracts becomes increasingly crucial. While some users are adept at reading code or the compiled bytecode to understand smart contracts, many rely on documentation. Therefore, discrepancies between the documentation and the deployed code can pose significant risks, whether these discrepancies are due to errors or intentional fraud. To tackle these challenges, we developed DeFiAligner, an end-to-end system to identify inconsistencies between documentation and smart contracts. DeFiAligner incorporates a symbolic execution tool, SEVM, which explores execution paths of on-chain binary code, recording memory and stack states. It automatically generates symbolic expressions for token balance changes and branch conditions, which, along with related project documents, are processed by LLMs. Using structured prompts, the LLMs evaluate the alignment between the symbolic expressions and the documentation. Our tests across three distinct scenarios demonstrate DeFiAligner’s capability to automate inconsistency detection in DeFi, achieving recall rates of 92% and 90% on two public datasets respectively.

Subject Classification

ACM Subject Classification
  • Security and privacy → Distributed systems security
Keywords
  • Decentralized Finance Security
  • Large Language Models
  • Project Review
  • Symbolic Analysis
  • Smart Contracts

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Bit-vector for go z3. URL: https://pkg.go.dev/github.com/aclements/go-z3/z3#BV.
  2. Contract abi specification. URL: https://docs.soliditylang.org/en/latest/abi-spec.html.
  3. Ethereum virtual machine (evm). URL: https://ethereum.org/en/developers/docs/evm/.
  4. Go-z3. URL: https://pkg.go.dev/github.com/aclements/go-z3/z3#section-documentation.
  5. Hack analysis: Uranium finance, april 2021. URL: https://medium.com/immunefi/building-a-poc-for-the-uranium-heist-ec83fbd83e9f.
  6. Introducing uni. URL: https://blog.uniswap.org/uni.
  7. Mythril. URL: https://github.com/ConsenSys/mythril.
  8. Openai. OpenAI. https://openai.com/. Google Scholar
  9. Uniswap. URL: https://uniswap.org/.
  10. What is an rpc node. URL: https://www.alchemy.com/overviews/rpc-node.
  11. Roberto Baldoni, Emilio Coppa, Daniele Cono D’elia, Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques. ACM Computing Surveys (CSUR), 51(3):1-39, 2018. Google Scholar
  12. Priyanka Bose, Dipanjan Das, Yanju Chen, Yu Feng, Christopher Kruegel, and Giovanni Vigna. Sailfish: Vetting smart contract state-inconsistency bugs in seconds. In 2022 IEEE Symposium on Security and Privacy (SP), pages 161-178. IEEE, 2022. Google Scholar
  13. Lexi Brent, Neville Grech, Sifis Lagouvardos, Bernhard Scholz, and Yannis Smaragdakis. Ethainter: a smart contract security analyzer for composite vulnerabilities. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 454-469, 2020. Google Scholar
  14. Lexi Brent, Anton Jurisevic, Michael Kong, Eric Liu, Francois Gauthier, Vincent Gramoli, Ralph Holz, and Bernhard Scholz. Vandal: A scalable security analysis framework for smart contracts. arXiv preprint arXiv:1809.03981, 2018. Google Scholar
  15. Vitalik Buterin. Vyper documentation. Vyper by Example, page 13, 2018. Google Scholar
  16. Stefanos Chaliasos, Marcos Antonios Charalambous, Liyi Zhou, Rafaila Galanopoulou, Arthur Gervais, Dimitris Mitropoulos, and Benjamin Livshits. Smart contract and defi security tools: Do they meet the needs of practitioners? In Proceedings of the 46th IEEE/ACM International Conference on Software Engineering, pages 1-13, 2024. Google Scholar
  17. Yupeng Chang, Xu Wang, Jindong Wang, Yuan Wu, Linyi Yang, Kaijie Zhu, Hao Chen, Xiaoyuan Yi, Cunxiang Wang, Yidong Wang, et al. A survey on evaluation of large language models. ACM Transactions on Intelligent Systems and Technology, 15(3):1-45, 2024. Google Scholar
  18. Ting Chen, Yufei Zhang, Zihao Li, Xiapu Luo, Ting Wang, Rong Cao, Xiuzhuo Xiao, and Xiaosong Zhang. Tokenscope: Automatically detecting inconsistent behaviors of cryptocurrency tokens in ethereum. In Proceedings of the 2019 ACM SIGSAC conference on computer and communications security, pages 1503-1520, 2019. Google Scholar
  19. Weimin Chen, Xinran Li, Yuting Sui, Ningyu He, Haoyu Wang, Lei Wu, and Xiapu Luo. Sadponzi: Detecting and characterizing ponzi schemes in ethereum smart contracts. Proceedings of the ACM on Measurement and Analysis of Computing Systems, 5(2):1-30, 2021. Google Scholar
  20. Weimin Chen, Xiapu Luo, Haoyu Wang, Heming Cui, Shuyu Zheng, and Xuanzhe Liu. Evmbt: A binary translation scheme for upgrading evm smart contracts to wasm. In Proceedings of the 25th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems, pages 131-142, 2024. Google Scholar
  21. Jaeseung Choi, Doyeon Kim, Soomin Kim, Gustavo Grieco, Alex Groce, and Sang Kil Cha. Smartian: Enhancing smart contract fuzzing with static and dynamic data-flow analyses. In 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 227-239. IEEE, 2021. Google Scholar
  22. Chris Dannen. Introducing Ethereum and solidity, volume 1. Springer, 2017. Google Scholar
  23. Isaac David, Liyi Zhou, Kaihua Qin, Dawn Song, Lorenzo Cavallaro, and Arthur Gervais. Do you still need a manual smart contract audit? arXiv preprint arXiv:2306.12338, 2023. Google Scholar
  24. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008. Google Scholar
  25. Josselin Feist, Gustavo Grieco, and Alex Groce. Slither: a static analysis framework for smart contracts. In 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), pages 8-15. IEEE, 2019. Google Scholar
  26. Yao Fu, Hao Peng, Litu Ou, Ashish Sabharwal, and Tushar Khot. Specializing smaller language models towards multi-step reasoning. In International Conference on Machine Learning, pages 10421-10430. PMLR, 2023. Google Scholar
  27. Yu Gai, Liyi Zhou, Kaihua Qin, Dawn Song, and Arthur Gervais. Blockchain large language models. arXiv preprint arXiv:2304.12749, 2023. Google Scholar
  28. Rundong Gan. DeFiAligner. Software, version 1.0., Natural Sciences and Engineering Research Council of Canada (NSERC), (visited on 2024-09-05). URL: https://github.com/DeFiAligner/DeFiAligner
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.22516
  29. Rundong Gan, Le Wang, and Xiaodong Lin. Why trick me: The honeypot traps on decentralized exchanges. In Proceedings of the 2023 Workshop on Decentralized Finance and Security, pages 17-23, 2023. Google Scholar
  30. Kanishk Gandhi, Jan-Philipp Fränken, Tobias Gerstenberg, and Noah Goodman. Understanding social reasoning in language models with language models. Advances in Neural Information Processing Systems, 36, 2024. Google Scholar
  31. Bingyu Gao, Haoyu Wang, Pengcheng Xia, Siwei Wu, Yajin Zhou, Xiapu Luo, and Gareth Tyson. Tracking counterfeit cryptocurrency end-to-end. Proceedings of the ACM on Measurement and Analysis of Computing Systems, 4(3):1-28, 2020. Google Scholar
  32. Neville Grech, Sifis Lagouvardos, Ilias Tsatiris, and Yannis Smaragdakis. Elipmoc: Advanced decompilation of ethereum smart contracts. Proceedings of the ACM on Programming Languages, 6(OOPSLA1):1-27, 2022. Google Scholar
  33. Sicheng Hao, Yuhong Nan, Zibin Zheng, and Xiaohui Liu. Smartcoco: Checking comment-code inconsistency in smart contracts via constraint propagation and binding. In 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 294-306. IEEE, 2023. Google Scholar
  34. Zheyuan He, Zihao Li, and Sen Yang. Large language models for blockchain security: A systematic literature review. arXiv preprint arXiv:2403.14280, 2024. Google Scholar
  35. Zheyuan He, Zhou Liao, Feng Luo, Dijun Liu, Ting Chen, and Zihao Li. Tokencat: detect flaw of authentication on erc20 tokens. In ICC 2022-IEEE International Conference on Communications, pages 4999-5004. IEEE, 2022. Google Scholar
  36. Zheyuan He, Shuwei Song, Yang Bai, Xiapu Luo, Ting Chen, Wensheng Zhang, Peng He, Hongwei Li, Xiaodong Lin, and Xiaosong Zhang. Tokenaware: Accurate and efficient bookkeeping recognition for token smart contracts. ACM Transactions on Software Engineering and Methodology, 32(1):1-35, 2023. Google Scholar
  37. Sihao Hu, Tiansheng Huang, Fatih İlhan, Selim Furkan Tekin, and Ling Liu. Large language model-powered smart contract vulnerability detection: New perspectives. arXiv preprint arXiv:2310.01152, 2023. Google Scholar
  38. Jie Huang and Kevin Chen-Chuan Chang. Towards reasoning in large language models: A survey. In 61st Annual Meeting of the Association for Computational Linguistics, ACL 2023, pages 1049-1065. Association for Computational Linguistics (ACL), 2023. Google Scholar
  39. Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. Zeus: analyzing safety of smart contracts. In Ndss, pages 1-12, 2018. Google Scholar
  40. James C King. Symbolic execution and program testing. Communications of the ACM, 19(7):385-394, 1976. Google Scholar
  41. Haonan Li, Yu Hao, Yizhuo Zhai, and Zhiyun Qian. Enhancing static analysis for practical bug detection: An llm-integrated approach. Proceedings of the ACM on Programming Languages, 8(OOPSLA1):474-499, 2024. Google Scholar
  42. Kai Li, Shixuan Guan, and Darren Lee. Towards understanding and characterizing the arbitrage bot scam in the wild. Proceedings of the ACM on Measurement and Analysis of Computing Systems, 7(3):1-29, 2023. Google Scholar
  43. Kaixuan Li, Yue Xue, Sen Chen, Han Liu, Kairan Sun, Ming Hu, Haijun Wang, Yang Liu, and Yixiang Chen. Static application security testing (sast) tools for smart contracts: How far are we? Proceedings of the ACM on Software Engineering, 1(FSE):1447-1470, 2024. Google Scholar
  44. Zewei Lin, Jiachi Chen, Jiajing Wu, Weizhe Zhang, Yongjuan Wang, and Zibin Zheng. Crpwarner: Warning the risk of contract-related rug pull in defi smart contracts. IEEE Transactions on Software Engineering, 2024. Google Scholar
  45. Ye Liu and Yi Li. Invcon: A dynamic invariant detector for ethereum smart contracts. In Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, pages 1-4, 2022. Google Scholar
  46. Ye Liu, Yue Xue, Daoyuan Wu, Yuqiang Sun, Yi Li, Miaolei Shi, and Yang Liu. Propertygpt: Llm-driven formal verification of smart contracts through retrieval-augmented property generation. arXiv preprint arXiv:2405.02580, 2024. Google Scholar
  47. Fuchen Ma, Meng Ren, Lerong Ouyang, Yuanliang Chen, Juan Zhu, Ting Chen, Yingli Zheng, Xiao Dai, Yu Jiang, and Jiaguang Sun. Pied-piper: Revealing the backdoor threats in ethereum erc token contracts. ACM Transactions on Software Engineering and Methodology, 32(3):1-24, 2023. Google Scholar
  48. Pengxiang Ma, Ningyu He, Yuhua Huang, Haoyu Wang, and Xiapu Luo. Abusing the ethereum smart contract verification services for fun and profit. arXiv preprint arXiv:2307.00549, 2023. Google Scholar
  49. Noble Saji Mathews, Yelizaveta Brus, Yousra Aafer, Mei Nagappan, and Shane McIntosh. Llbezpeky: Leveraging large language models for vulnerability detection. arXiv preprint arXiv:2401.01269, 2024. Google Scholar
  50. Alexander Mense and Markus Flatscher. Security vulnerabilities in ethereum smart contracts. In Proceedings of the 20th international conference on information integration and web-based applications & services, pages 375-380, 2018. Google Scholar
  51. Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, and Artem Dinaburg. Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. In 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 1186-1189. IEEE, 2019. Google Scholar
  52. Tai D Nguyen, Long H Pham, Jun Sun, Yun Lin, and Quang Tran Minh. sfuzz: An efficient adaptive fuzzer for solidity smart contracts. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, pages 778-788, 2020. Google Scholar
  53. Jack Nicholls, Aditya Kuppa, and Nhien-An Le-Khac. Enhancing illicit activity detection using xai: A multimodal graph-llm framework. arXiv preprint arXiv:2310.13787, 2023. Google Scholar
  54. Kaihua Qin, Liyi Zhou, Yaroslav Afonin, Ludovico Lazzaretti, and Arthur Gervais. Cefi vs. defi-comparing centralized to decentralized finance. arXiv preprint arXiv:2106.08157, 2021. Google Scholar
  55. Sanka Rasnayaka, Guanlin Wang, Ridwan Shariffdeen, and Ganesh Neelakanta Iyer. An empirical study on usage and perceptions of llms in a software engineering project. arXiv preprint arXiv:2401.16186, 2024. Google Scholar
  56. Abulhair Saparov, Richard Yuanzhe Pang, Vishakh Padmakumar, Nitish Joshi, Mehran Kazemi, Najoung Kim, and He He. Testing the general deductive reasoning capacity of large language models using ood examples. Advances in Neural Information Processing Systems, 36, 2024. Google Scholar
  57. Shiwen Shan, Yintong Huo, Yuxin Su, Yichen Li, Dan Li, and Zibin Zheng. Face it yourselves: An llm-based two-stage strategy to localize configuration errors via logs. arXiv preprint arXiv:2404.00640, 2024. Google Scholar
  58. Chaofan Shou, Jing Liu, Doudou Lu, and Koushik Sen. Llm4fuzz: Guided fuzzing of smart contracts with large language models. arXiv preprint arXiv:2401.11108, 2024. Google Scholar
  59. Tianle Sun, Ningyu He, Jiang Xiao, Yinliang Yue, Xiapu Luo, and Haoyu Wang. All your tokens are belong to us: Demystifying address verification vulnerabilities in solidity smart contracts. arXiv preprint arXiv:2405.20561, 2024. Google Scholar
  60. Yuqiang Sun, Daoyuan Wu, Yue Xue, Han Liu, Wei Ma, Lyuye Zhang, Miaolei Shi, and Yang Liu. Llm4vuln: A unified evaluation framework for decoupling and enhancing llms' vulnerability reasoning. arXiv preprint arXiv:2401.16185, 2024. Google Scholar
  61. Yuqiang Sun, Daoyuan Wu, Yue Xue, Han Liu, Haijun Wang, Zhengzi Xu, Xiaofei Xie, and Yang Liu. Gptscan: Detecting logic vulnerabilities in smart contracts by combining gpt with program analysis. In Proceedings of the IEEE/ACM 46th International Conference on Software Engineering, pages 1-13, 2024. Google Scholar
  62. Robert Tarjan. Depth-first search and linear graph algorithms. SIAM journal on computing, 1(2):146-160, 1972. Google Scholar
  63. Sergei Tikhomirov, Ekaterina Voskresenskaya, Ivan Ivanitskiy, Ramil Takhaviev, Evgeny Marchenko, and Yaroslav Alexandrov. Smartcheck: Static analysis of ethereum smart contracts. In Proceedings of the 1st international workshop on emerging trends in software engineering for blockchain, pages 9-16, 2018. Google Scholar
  64. Christof Ferreira Torres, Antonio Ken Iannillo, Arthur Gervais, and Radu State. Confuzzius: A data dependency-aware hybrid fuzzer for smart contracts. In 2021 IEEE European Symposium on Security and Privacy (EuroS&P), pages 103-119. IEEE, 2021. Google Scholar
  65. Christof Ferreira Torres, Julian Schütte, and Radu State. Osiris: Hunting for integer bugs in ethereum smart contracts. In Proceedings of the 34th annual computer security applications conference, pages 664-676, 2018. Google Scholar
  66. Petar Tsankov, Andrei Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Buenzli, and Martin Vechev. Securify: Practical security analysis of smart contracts. In Proceedings of the 2018 ACM SIGSAC conference on computer and communications security, pages 67-82, 2018. Google Scholar
  67. Junjie Wang, Yuchao Huang, Chunyang Chen, Zhe Liu, Song Wang, and Qing Wang. Software testing with large language models: Survey, landscape, and vision. IEEE Transactions on Software Engineering, 2024. Google Scholar
  68. Sally Junsong Wang, Kexin Pei, and Junfeng Yang. Smartinv: Multimodal learning for smart contract invariant inference. In 2024 IEEE Symposium on Security and Privacy (SP), pages 126-126. IEEE Computer Society, 2024. Google Scholar
  69. Yiqi Wang, Wentao Chen, Xiaotian Han, Xudong Lin, Haiteng Zhao, Yongfei Liu, Bohan Zhai, Jianbo Yuan, Quanzeng You, and Hongxia Yang. Exploring the reasoning abilities of multimodal large language models (mllms): A comprehensive survey on emerging trends in multimodal reasoning. arXiv preprint arXiv:2401.06805, 2024. Google Scholar
  70. Zexu Wang, Jiachi Chen, Yanlin Wang, Yu Zhang, Weizhe Zhang, and Zibin Zheng. Efficiently detecting reentrancy vulnerabilities in complex smart contracts. arXiv preprint arXiv:2403.11254, 2024. Google Scholar
  71. Gavin Wood et al. Ethereum: A secure decentralised generalised transaction ledger. Ethereum project yellow paper, 151(2014):1-32, 2014. Google Scholar
  72. Tianyu Wu, Shizhu He, Jingping Liu, Siqi Sun, Kang Liu, Qing-Long Han, and Yang Tang. A brief overview of chatgpt: The history, status quo and potential future development. IEEE/CAA Journal of Automatica Sinica, 10(5):1122-1136, 2023. Google Scholar
  73. Pengcheng Xia, Haoyu Wang, Bingyu Gao, Weihang Su, Zhou Yu, Xiapu Luo, Chao Zhang, Xusheng Xiao, and Guoai Xu. Trade or trick? detecting and characterizing scam tokens on uniswap decentralized exchange. Proceedings of the ACM on Measurement and Analysis of Computing Systems, 5(3):1-26, 2021. Google Scholar
  74. Jingfeng Yang, Hongye Jin, Ruixiang Tang, Xiaotian Han, Qizhang Feng, Haoming Jiang, Shaochen Zhong, Bing Yin, and Xia Hu. Harnessing the power of llms in practice: A survey on chatgpt and beyond. ACM Transactions on Knowledge Discovery from Data, 18(6):1-32, 2024. Google Scholar
  75. Lei Yu, Junyi Lu, Xianglong Liu, Li Yang, Fengjun Zhang, and Jiajia Ma. Pscvfinder: A prompt-tuning based framework for smart contract vulnerability detection. In 2023 IEEE 34th International Symposium on Software Reliability Engineering (ISSRE), pages 556-567. IEEE, 2023. Google Scholar
  76. Lyuye Zhang, Kaixuan Li, Kairan Sun, Daoyuan Wu, Ye Liu, Haoye Tian, and Yang Liu. Acfix: Guiding llms with mined common rbac practices for context-aware repair of access control vulnerabilities in smart contracts. arXiv preprint arXiv:2403.06838, 2024. Google Scholar
  77. Wayne Xin Zhao, Kun Zhou, Junyi Li, Tianyi Tang, Xiaolei Wang, Yupeng Hou, Yingqian Min, Beichen Zhang, Junjie Zhang, Zican Dong, et al. A survey of large language models. arXiv preprint arXiv:2303.18223, 2023. Google Scholar
  78. Zibin Zheng, Shaoan Xie, Hong-Ning Dai, Weili Chen, Xiangping Chen, Jian Weng, and Muhammad Imran. An overview on smart contracts: Challenges, advances and platforms. Future Generation Computer Systems, 105:475-491, 2020. Google Scholar
  79. Zibin Zheng, Shaoan Xie, Hongning Dai, Xiangping Chen, and Huaimin Wang. An overview of blockchain technology: Architecture, consensus, and future trends. In 2017 IEEE international congress on big data (BigData congress), pages 557-564. Ieee, 2017. Google Scholar
  80. Jianfei Zhou, Tianxing Jiang, Haijun Wang, Meng Wu, and Ting Chen. Dapphunter: Identifying inconsistent behaviors of blockchain-based decentralized applications. In 2023 IEEE/ACM 45th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP), pages 24-35. IEEE, 2023. Google Scholar
  81. Yuanhang Zhou, Jingxuan Sun, Fuchen Ma, Yuanliang Chen, Zhen Yan, and Yu Jiang. Stop pulling my rug: Exposing rug pull risks in crypto token to investors. In Proceedings of the 46th International Conference on Software Engineering: Software Engineering in Practice ICSE-SEIP, pages 228-239. ACM, 2024. Google Scholar
  82. Chenguang Zhu, Ye Liu, Xiuheng Wu, and Yi Li. Identifying solidity smart contract api documentation errors. In Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, pages 1-13, 2022. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact