Workshop SOAP 2022 – Author Index |
Contents -
Abstracts -
Authors
|
A B C D F G J K L M N O R S T W
Anteski, Naum |
SOAP '22: "ADA: A Tool for Visualizing ..."
ADA: A Tool for Visualizing the Architectural Overview of Open-Source Repositories
Md Rakib Hossain Misu, Aleksandar Saša Janjanin, Zhiqiang Bian, Valentin-Sebastian Burlacu, and Naum Anteski (University College London, UK) Writing highly maintainable and efficient software code is becoming increasingly difficult, especially while following the rapid, agile development process and working in a distributed team. One of the key indicators of that inefficient software design is a high degree of code coupling, which leads to unwanted side-effects during refactoring and acts as a burden during future development. To alleviate these problems, we developed a visualization tool, ADA, that statically analyzes an open-source repository and seeks to address the issue of code coupling by providing developers with a powerful graphic representation. ADA showcases the relationships and the degree of inter-connectivity between the classes. ADA will ultimately guide developers to instantly locate the coupled area and assist them in decoupling it. @InProceedings{SOAP22p30, author = {Md Rakib Hossain Misu and Aleksandar Saša Janjanin and Zhiqiang Bian and Valentin-Sebastian Burlacu and Naum Anteski}, title = {ADA: A Tool for Visualizing the Architectural Overview of Open-Source Repositories}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {30--35}, doi = {10.1145/3520313.3534659}, year = {2022}, } Publisher's Version |
|
Arceri, Vincenzo |
SOAP '22: "Ensuring Determinism in Blockchain ..."
Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report
Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, and Enrico Talin (University of Verona, Italy; Corvallis, Italy; Commercio.network, Italy; University of Parma, Italy; Ca' Foscari University of Venice, Italy) Ensuring determinism is mandatory when writing blockchain software. When determinism is not met it can lead to serious implications in the blockchain network while compromising the software development, release, and patching processes. In the industrial context, it is widespread to adopt general-purpose languages, such as Go, for developing blockchain solutions. However, it is not surprising that non-deterministic behaviors may arise, being these programming languages not originally designed for blockchain purposes. In this paper, we present an experience report on ensuring determinism in blockchain software with GoLiSA, a static analyzer based on abstract interpretation for Go applications, in an industrial context. In particular, we ran GoLiSA on Commercio.network, a blockchain-based solution for exchanging electronic documents in a legally binding way. Thanks to GoLiSA, non-trivial bugs got detected and the analysis performed made it possible to identify the critical points where to apply the fixes. @InProceedings{SOAP22p23, author = {Luca Olivieri and Fabio Tagliaferro and Vincenzo Arceri and Marco Ruaro and Luca Negrini and Agostino Cortesi and Pietro Ferrara and Fausto Spoto and Enrico Talin}, title = {Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {23--29}, doi = {10.1145/3520313.3534658}, year = {2022}, } Publisher's Version |
|
Balachandran, Swee |
SOAP '22: "Towards an Implementation ..."
Towards an Implementation of Differential Dynamic Logic in PVS
J. Tanner Slagel, César Muñoz, Swee Balachandran, Mariano Moscato, Aaron Dutle, Paolo Masci, and Lauren White (NASA Langley Research Center, USA; National Institute of Aerospace, USA) This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, i.e., systems that employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and inference rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification of hybrid systems. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties. @InProceedings{SOAP22p44, author = {J. Tanner Slagel and César Muñoz and Swee Balachandran and Mariano Moscato and Aaron Dutle and Paolo Masci and Lauren White}, title = {Towards an Implementation of Differential Dynamic Logic in PVS}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {44--50}, doi = {10.1145/3520313.3534661}, year = {2022}, } Publisher's Version |
|
Bau, Guillaume |
SOAP '22: "Abstract Interpretation of ..."
Abstract Interpretation of Michelson Smart-Contracts
Guillaume Bau, Antoine Miné, Vincent Botbol, and Mehdi Bouaziz (Sorbonne University, France; CNRS, France; LIP6, France; Nomadic Labs, France) Static analysis of smart-contracts is becoming more widespread on blockchain platforms. Analyzers rely on techniques like symbolic execution or model checking, but few of them can provide strong soundness properties and guarantee the analysis termination at the same time. As smart-contracts often manipulate economic assets, proving numerical properties beyond the absence of runtime errors is also desirable. Smart-contract execution models differ considerably from mainstream programming languages and vary from one blockchain to another, making state-of-the-art analyses hard to adapt. For instance, smart-contract calls may modify a persistent storage impacting subsequent calls. This makes it difficult for tools to infer invariants %and high-level security properties required to formally ensure the absence of exploitable vulnerabilities. The Michelson smart-contract language, used in the Tezos blockchain, is strongly typed, stack-based, and has a strict execution model leaving few opportunities for implicit runtime errors. We present a work in progress static analyzer for Michelson based on Abstract Interpretation and implemented within MOPSA, a modular static analyzer. Our tool supports the Michelson semantic features, including inner calls to external contracts. It can prove the absence of runtime errors and infer invariants on the persistent storage over an unbounded number of calls. It is also being extended to prove high-level numerical and security properties. @InProceedings{SOAP22p36, author = {Guillaume Bau and Antoine Miné and Vincent Botbol and Mehdi Bouaziz}, title = {Abstract Interpretation of Michelson Smart-Contracts}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {36--43}, doi = {10.1145/3520313.3534660}, year = {2022}, } Publisher's Version Archive submitted (8.2 kB) |
|
Bian, Zhiqiang |
SOAP '22: "ADA: A Tool for Visualizing ..."
ADA: A Tool for Visualizing the Architectural Overview of Open-Source Repositories
Md Rakib Hossain Misu, Aleksandar Saša Janjanin, Zhiqiang Bian, Valentin-Sebastian Burlacu, and Naum Anteski (University College London, UK) Writing highly maintainable and efficient software code is becoming increasingly difficult, especially while following the rapid, agile development process and working in a distributed team. One of the key indicators of that inefficient software design is a high degree of code coupling, which leads to unwanted side-effects during refactoring and acts as a burden during future development. To alleviate these problems, we developed a visualization tool, ADA, that statically analyzes an open-source repository and seeks to address the issue of code coupling by providing developers with a powerful graphic representation. ADA showcases the relationships and the degree of inter-connectivity between the classes. ADA will ultimately guide developers to instantly locate the coupled area and assist them in decoupling it. @InProceedings{SOAP22p30, author = {Md Rakib Hossain Misu and Aleksandar Saša Janjanin and Zhiqiang Bian and Valentin-Sebastian Burlacu and Naum Anteski}, title = {ADA: A Tool for Visualizing the Architectural Overview of Open-Source Repositories}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {30--35}, doi = {10.1145/3520313.3534659}, year = {2022}, } Publisher's Version |
|
Bojanić, Uroš |
SOAP '22: "Statically Detecting Data ..."
Statically Detecting Data Leakages in Data Science Code
Pavle Subotić, Uroš Bojanić, and Milan Stojić (Microsoft, Serbia) Data leakage is a well-known problem in machine learning. Data leakage occurs when information from outside the training dataset is used to create a model. This phenomenon renders a model excessively optimistic or even useless in the real world since the model tends to leverage greatly on the unfairly acquired information. To date, detection of data leakages occurs post-mortem using runtime methods. In this paper, we develop a static data leakage analysis to detect several instances of data leakages during development time. Our analysis is constructed to be lightweight so that it can be performed within interactive data science notebooks. We have integrated our analysis into the NBLyzer static analyzer framework and show its utility on real world benchmarks. To the best of our knowledge, we propose the first static detection of data science data leakages. @InProceedings{SOAP22p16, author = {Pavle Subotić and Uroš Bojanić and Milan Stojić}, title = {Statically Detecting Data Leakages in Data Science Code}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {16--22}, doi = {10.1145/3520313.3534657}, year = {2022}, } Publisher's Version |
|
Botbol, Vincent |
SOAP '22: "Abstract Interpretation of ..."
Abstract Interpretation of Michelson Smart-Contracts
Guillaume Bau, Antoine Miné, Vincent Botbol, and Mehdi Bouaziz (Sorbonne University, France; CNRS, France; LIP6, France; Nomadic Labs, France) Static analysis of smart-contracts is becoming more widespread on blockchain platforms. Analyzers rely on techniques like symbolic execution or model checking, but few of them can provide strong soundness properties and guarantee the analysis termination at the same time. As smart-contracts often manipulate economic assets, proving numerical properties beyond the absence of runtime errors is also desirable. Smart-contract execution models differ considerably from mainstream programming languages and vary from one blockchain to another, making state-of-the-art analyses hard to adapt. For instance, smart-contract calls may modify a persistent storage impacting subsequent calls. This makes it difficult for tools to infer invariants %and high-level security properties required to formally ensure the absence of exploitable vulnerabilities. The Michelson smart-contract language, used in the Tezos blockchain, is strongly typed, stack-based, and has a strict execution model leaving few opportunities for implicit runtime errors. We present a work in progress static analyzer for Michelson based on Abstract Interpretation and implemented within MOPSA, a modular static analyzer. Our tool supports the Michelson semantic features, including inner calls to external contracts. It can prove the absence of runtime errors and infer invariants on the persistent storage over an unbounded number of calls. It is also being extended to prove high-level numerical and security properties. @InProceedings{SOAP22p36, author = {Guillaume Bau and Antoine Miné and Vincent Botbol and Mehdi Bouaziz}, title = {Abstract Interpretation of Michelson Smart-Contracts}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {36--43}, doi = {10.1145/3520313.3534660}, year = {2022}, } Publisher's Version Archive submitted (8.2 kB) |
|
Bouaziz, Mehdi |
SOAP '22: "Abstract Interpretation of ..."
Abstract Interpretation of Michelson Smart-Contracts
Guillaume Bau, Antoine Miné, Vincent Botbol, and Mehdi Bouaziz (Sorbonne University, France; CNRS, France; LIP6, France; Nomadic Labs, France) Static analysis of smart-contracts is becoming more widespread on blockchain platforms. Analyzers rely on techniques like symbolic execution or model checking, but few of them can provide strong soundness properties and guarantee the analysis termination at the same time. As smart-contracts often manipulate economic assets, proving numerical properties beyond the absence of runtime errors is also desirable. Smart-contract execution models differ considerably from mainstream programming languages and vary from one blockchain to another, making state-of-the-art analyses hard to adapt. For instance, smart-contract calls may modify a persistent storage impacting subsequent calls. This makes it difficult for tools to infer invariants %and high-level security properties required to formally ensure the absence of exploitable vulnerabilities. The Michelson smart-contract language, used in the Tezos blockchain, is strongly typed, stack-based, and has a strict execution model leaving few opportunities for implicit runtime errors. We present a work in progress static analyzer for Michelson based on Abstract Interpretation and implemented within MOPSA, a modular static analyzer. Our tool supports the Michelson semantic features, including inner calls to external contracts. It can prove the absence of runtime errors and infer invariants on the persistent storage over an unbounded number of calls. It is also being extended to prove high-level numerical and security properties. @InProceedings{SOAP22p36, author = {Guillaume Bau and Antoine Miné and Vincent Botbol and Mehdi Bouaziz}, title = {Abstract Interpretation of Michelson Smart-Contracts}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {36--43}, doi = {10.1145/3520313.3534660}, year = {2022}, } Publisher's Version Archive submitted (8.2 kB) |
|
Burlacu, Valentin-Sebastian |
SOAP '22: "ADA: A Tool for Visualizing ..."
ADA: A Tool for Visualizing the Architectural Overview of Open-Source Repositories
Md Rakib Hossain Misu, Aleksandar Saša Janjanin, Zhiqiang Bian, Valentin-Sebastian Burlacu, and Naum Anteski (University College London, UK) Writing highly maintainable and efficient software code is becoming increasingly difficult, especially while following the rapid, agile development process and working in a distributed team. One of the key indicators of that inefficient software design is a high degree of code coupling, which leads to unwanted side-effects during refactoring and acts as a burden during future development. To alleviate these problems, we developed a visualization tool, ADA, that statically analyzes an open-source repository and seeks to address the issue of code coupling by providing developers with a powerful graphic representation. ADA showcases the relationships and the degree of inter-connectivity between the classes. ADA will ultimately guide developers to instantly locate the coupled area and assist them in decoupling it. @InProceedings{SOAP22p30, author = {Md Rakib Hossain Misu and Aleksandar Saša Janjanin and Zhiqiang Bian and Valentin-Sebastian Burlacu and Naum Anteski}, title = {ADA: A Tool for Visualizing the Architectural Overview of Open-Source Repositories}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {30--35}, doi = {10.1145/3520313.3534659}, year = {2022}, } Publisher's Version |
|
Cortesi, Agostino |
SOAP '22: "Ensuring Determinism in Blockchain ..."
Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report
Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, and Enrico Talin (University of Verona, Italy; Corvallis, Italy; Commercio.network, Italy; University of Parma, Italy; Ca' Foscari University of Venice, Italy) Ensuring determinism is mandatory when writing blockchain software. When determinism is not met it can lead to serious implications in the blockchain network while compromising the software development, release, and patching processes. In the industrial context, it is widespread to adopt general-purpose languages, such as Go, for developing blockchain solutions. However, it is not surprising that non-deterministic behaviors may arise, being these programming languages not originally designed for blockchain purposes. In this paper, we present an experience report on ensuring determinism in blockchain software with GoLiSA, a static analyzer based on abstract interpretation for Go applications, in an industrial context. In particular, we ran GoLiSA on Commercio.network, a blockchain-based solution for exchanging electronic documents in a legally binding way. Thanks to GoLiSA, non-trivial bugs got detected and the analysis performed made it possible to identify the critical points where to apply the fixes. @InProceedings{SOAP22p23, author = {Luca Olivieri and Fabio Tagliaferro and Vincenzo Arceri and Marco Ruaro and Luca Negrini and Agostino Cortesi and Pietro Ferrara and Fausto Spoto and Enrico Talin}, title = {Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {23--29}, doi = {10.1145/3520313.3534658}, year = {2022}, } Publisher's Version |
|
Debray, Saumya |
SOAP '22: "Modeling Code Manipulation ..."
Modeling Code Manipulation in JIT Compilers
HeuiChan Lim, Xiyu Kang, and Saumya Debray (University of Arizona, USA) Just-in-Time (JIT) compilers are widely used to improve the performance of interpreter-based language implementations by creating optimized code at runtime. However, bugs in the JIT compiler’s code manipulation and optimization can result in the generation of incorrect code. Such bugs can be difficult to diagnose and fix, and can result in exploitable vulnerabilities. Unfortunately, existing approaches to automatic bug localization do not carry over well to such bugs. This paper discusses a different approach to analyzing JIT compiler optimization behaviors, based on using dynamic analysis to construct abstract models of the JIT compiler’s optimizer and back end. By comparing the models obtained for buggy and non-buggy executions of the JIT compiler, we can pinpoint the components of the JIT compiler’s internal representation that have been affected by the bug; this can then be mapped back to identify the buggy code. Our experiments with two real bugs for Google V8 JIT compiler, TurboFan, show the utility and practicality of our approach. @InProceedings{SOAP22p9, author = {HeuiChan Lim and Xiyu Kang and Saumya Debray}, title = {Modeling Code Manipulation in JIT Compilers}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {9--15}, doi = {10.1145/3520313.3534656}, year = {2022}, } Publisher's Version |
|
Dutle, Aaron |
SOAP '22: "Towards an Implementation ..."
Towards an Implementation of Differential Dynamic Logic in PVS
J. Tanner Slagel, César Muñoz, Swee Balachandran, Mariano Moscato, Aaron Dutle, Paolo Masci, and Lauren White (NASA Langley Research Center, USA; National Institute of Aerospace, USA) This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, i.e., systems that employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and inference rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification of hybrid systems. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties. @InProceedings{SOAP22p44, author = {J. Tanner Slagel and César Muñoz and Swee Balachandran and Mariano Moscato and Aaron Dutle and Paolo Masci and Lauren White}, title = {Towards an Implementation of Differential Dynamic Logic in PVS}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {44--50}, doi = {10.1145/3520313.3534661}, year = {2022}, } Publisher's Version |
|
Ferrara, Pietro |
SOAP '22: "Ensuring Determinism in Blockchain ..."
Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report
Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, and Enrico Talin (University of Verona, Italy; Corvallis, Italy; Commercio.network, Italy; University of Parma, Italy; Ca' Foscari University of Venice, Italy) Ensuring determinism is mandatory when writing blockchain software. When determinism is not met it can lead to serious implications in the blockchain network while compromising the software development, release, and patching processes. In the industrial context, it is widespread to adopt general-purpose languages, such as Go, for developing blockchain solutions. However, it is not surprising that non-deterministic behaviors may arise, being these programming languages not originally designed for blockchain purposes. In this paper, we present an experience report on ensuring determinism in blockchain software with GoLiSA, a static analyzer based on abstract interpretation for Go applications, in an industrial context. In particular, we ran GoLiSA on Commercio.network, a blockchain-based solution for exchanging electronic documents in a legally binding way. Thanks to GoLiSA, non-trivial bugs got detected and the analysis performed made it possible to identify the critical points where to apply the fixes. @InProceedings{SOAP22p23, author = {Luca Olivieri and Fabio Tagliaferro and Vincenzo Arceri and Marco Ruaro and Luca Negrini and Agostino Cortesi and Pietro Ferrara and Fausto Spoto and Enrico Talin}, title = {Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {23--29}, doi = {10.1145/3520313.3534658}, year = {2022}, } Publisher's Version |
|
Gopalakrishnan, Ganesh |
SOAP '22: "BinFPE: Accurate Floating-Point ..."
BinFPE: Accurate Floating-Point Exception Detection for GPU Applications
Ignacio Laguna, Xinyi Li, and Ganesh Gopalakrishnan (Lawrence Livermore National Laboratory, USA; University of Utah, USA) When modern heterogeneous HPC systems perform numerical computations, floating-point exceptional quantities such as NaN and infinity in the GPU context, remain insufficiently handled. This is because commonly used GPUs and the CUDA language have no inherent exception detection capabilities. Existing compiler-based approaches for this problem are tied to a given compiler and cannot detect exceptions generated by binaries and precompiled libraries. This paper contributes BinFPE, a unique tool that addresses these challenges. BinFPE uses the NVBit dynamic binary instrumentation framework to check the machine registers after each calculation to recognize exceptions, and conveys this information to the CPU for final reporting. We demonstrate the effectiveness of BinFPE on 42 CUDA programs, reporting previously unreported exceptions. We also present the limitations of BinFPE and our perspective on building GPU tools via binary instrumentation. @InProceedings{SOAP22p1, author = {Ignacio Laguna and Xinyi Li and Ganesh Gopalakrishnan}, title = {BinFPE: Accurate Floating-Point Exception Detection for GPU Applications}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {1--8}, doi = {10.1145/3520313.3534655}, year = {2022}, } Publisher's Version |
|
Janjanin, Aleksandar Saša |
SOAP '22: "ADA: A Tool for Visualizing ..."
ADA: A Tool for Visualizing the Architectural Overview of Open-Source Repositories
Md Rakib Hossain Misu, Aleksandar Saša Janjanin, Zhiqiang Bian, Valentin-Sebastian Burlacu, and Naum Anteski (University College London, UK) Writing highly maintainable and efficient software code is becoming increasingly difficult, especially while following the rapid, agile development process and working in a distributed team. One of the key indicators of that inefficient software design is a high degree of code coupling, which leads to unwanted side-effects during refactoring and acts as a burden during future development. To alleviate these problems, we developed a visualization tool, ADA, that statically analyzes an open-source repository and seeks to address the issue of code coupling by providing developers with a powerful graphic representation. ADA showcases the relationships and the degree of inter-connectivity between the classes. ADA will ultimately guide developers to instantly locate the coupled area and assist them in decoupling it. @InProceedings{SOAP22p30, author = {Md Rakib Hossain Misu and Aleksandar Saša Janjanin and Zhiqiang Bian and Valentin-Sebastian Burlacu and Naum Anteski}, title = {ADA: A Tool for Visualizing the Architectural Overview of Open-Source Repositories}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {30--35}, doi = {10.1145/3520313.3534659}, year = {2022}, } Publisher's Version |
|
Kang, Xiyu |
SOAP '22: "Modeling Code Manipulation ..."
Modeling Code Manipulation in JIT Compilers
HeuiChan Lim, Xiyu Kang, and Saumya Debray (University of Arizona, USA) Just-in-Time (JIT) compilers are widely used to improve the performance of interpreter-based language implementations by creating optimized code at runtime. However, bugs in the JIT compiler’s code manipulation and optimization can result in the generation of incorrect code. Such bugs can be difficult to diagnose and fix, and can result in exploitable vulnerabilities. Unfortunately, existing approaches to automatic bug localization do not carry over well to such bugs. This paper discusses a different approach to analyzing JIT compiler optimization behaviors, based on using dynamic analysis to construct abstract models of the JIT compiler’s optimizer and back end. By comparing the models obtained for buggy and non-buggy executions of the JIT compiler, we can pinpoint the components of the JIT compiler’s internal representation that have been affected by the bug; this can then be mapped back to identify the buggy code. Our experiments with two real bugs for Google V8 JIT compiler, TurboFan, show the utility and practicality of our approach. @InProceedings{SOAP22p9, author = {HeuiChan Lim and Xiyu Kang and Saumya Debray}, title = {Modeling Code Manipulation in JIT Compilers}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {9--15}, doi = {10.1145/3520313.3534656}, year = {2022}, } Publisher's Version |
|
Laguna, Ignacio |
SOAP '22: "BinFPE: Accurate Floating-Point ..."
BinFPE: Accurate Floating-Point Exception Detection for GPU Applications
Ignacio Laguna, Xinyi Li, and Ganesh Gopalakrishnan (Lawrence Livermore National Laboratory, USA; University of Utah, USA) When modern heterogeneous HPC systems perform numerical computations, floating-point exceptional quantities such as NaN and infinity in the GPU context, remain insufficiently handled. This is because commonly used GPUs and the CUDA language have no inherent exception detection capabilities. Existing compiler-based approaches for this problem are tied to a given compiler and cannot detect exceptions generated by binaries and precompiled libraries. This paper contributes BinFPE, a unique tool that addresses these challenges. BinFPE uses the NVBit dynamic binary instrumentation framework to check the machine registers after each calculation to recognize exceptions, and conveys this information to the CPU for final reporting. We demonstrate the effectiveness of BinFPE on 42 CUDA programs, reporting previously unreported exceptions. We also present the limitations of BinFPE and our perspective on building GPU tools via binary instrumentation. @InProceedings{SOAP22p1, author = {Ignacio Laguna and Xinyi Li and Ganesh Gopalakrishnan}, title = {BinFPE: Accurate Floating-Point Exception Detection for GPU Applications}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {1--8}, doi = {10.1145/3520313.3534655}, year = {2022}, } Publisher's Version |
|
Lim, HeuiChan |
SOAP '22: "Modeling Code Manipulation ..."
Modeling Code Manipulation in JIT Compilers
HeuiChan Lim, Xiyu Kang, and Saumya Debray (University of Arizona, USA) Just-in-Time (JIT) compilers are widely used to improve the performance of interpreter-based language implementations by creating optimized code at runtime. However, bugs in the JIT compiler’s code manipulation and optimization can result in the generation of incorrect code. Such bugs can be difficult to diagnose and fix, and can result in exploitable vulnerabilities. Unfortunately, existing approaches to automatic bug localization do not carry over well to such bugs. This paper discusses a different approach to analyzing JIT compiler optimization behaviors, based on using dynamic analysis to construct abstract models of the JIT compiler’s optimizer and back end. By comparing the models obtained for buggy and non-buggy executions of the JIT compiler, we can pinpoint the components of the JIT compiler’s internal representation that have been affected by the bug; this can then be mapped back to identify the buggy code. Our experiments with two real bugs for Google V8 JIT compiler, TurboFan, show the utility and practicality of our approach. @InProceedings{SOAP22p9, author = {HeuiChan Lim and Xiyu Kang and Saumya Debray}, title = {Modeling Code Manipulation in JIT Compilers}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {9--15}, doi = {10.1145/3520313.3534656}, year = {2022}, } Publisher's Version |
|
Li, Xinyi |
SOAP '22: "BinFPE: Accurate Floating-Point ..."
BinFPE: Accurate Floating-Point Exception Detection for GPU Applications
Ignacio Laguna, Xinyi Li, and Ganesh Gopalakrishnan (Lawrence Livermore National Laboratory, USA; University of Utah, USA) When modern heterogeneous HPC systems perform numerical computations, floating-point exceptional quantities such as NaN and infinity in the GPU context, remain insufficiently handled. This is because commonly used GPUs and the CUDA language have no inherent exception detection capabilities. Existing compiler-based approaches for this problem are tied to a given compiler and cannot detect exceptions generated by binaries and precompiled libraries. This paper contributes BinFPE, a unique tool that addresses these challenges. BinFPE uses the NVBit dynamic binary instrumentation framework to check the machine registers after each calculation to recognize exceptions, and conveys this information to the CPU for final reporting. We demonstrate the effectiveness of BinFPE on 42 CUDA programs, reporting previously unreported exceptions. We also present the limitations of BinFPE and our perspective on building GPU tools via binary instrumentation. @InProceedings{SOAP22p1, author = {Ignacio Laguna and Xinyi Li and Ganesh Gopalakrishnan}, title = {BinFPE: Accurate Floating-Point Exception Detection for GPU Applications}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {1--8}, doi = {10.1145/3520313.3534655}, year = {2022}, } Publisher's Version |
|
Masci, Paolo |
SOAP '22: "Towards an Implementation ..."
Towards an Implementation of Differential Dynamic Logic in PVS
J. Tanner Slagel, César Muñoz, Swee Balachandran, Mariano Moscato, Aaron Dutle, Paolo Masci, and Lauren White (NASA Langley Research Center, USA; National Institute of Aerospace, USA) This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, i.e., systems that employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and inference rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification of hybrid systems. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties. @InProceedings{SOAP22p44, author = {J. Tanner Slagel and César Muñoz and Swee Balachandran and Mariano Moscato and Aaron Dutle and Paolo Masci and Lauren White}, title = {Towards an Implementation of Differential Dynamic Logic in PVS}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {44--50}, doi = {10.1145/3520313.3534661}, year = {2022}, } Publisher's Version |
|
Miné, Antoine |
SOAP '22: "Abstract Interpretation of ..."
Abstract Interpretation of Michelson Smart-Contracts
Guillaume Bau, Antoine Miné, Vincent Botbol, and Mehdi Bouaziz (Sorbonne University, France; CNRS, France; LIP6, France; Nomadic Labs, France) Static analysis of smart-contracts is becoming more widespread on blockchain platforms. Analyzers rely on techniques like symbolic execution or model checking, but few of them can provide strong soundness properties and guarantee the analysis termination at the same time. As smart-contracts often manipulate economic assets, proving numerical properties beyond the absence of runtime errors is also desirable. Smart-contract execution models differ considerably from mainstream programming languages and vary from one blockchain to another, making state-of-the-art analyses hard to adapt. For instance, smart-contract calls may modify a persistent storage impacting subsequent calls. This makes it difficult for tools to infer invariants %and high-level security properties required to formally ensure the absence of exploitable vulnerabilities. The Michelson smart-contract language, used in the Tezos blockchain, is strongly typed, stack-based, and has a strict execution model leaving few opportunities for implicit runtime errors. We present a work in progress static analyzer for Michelson based on Abstract Interpretation and implemented within MOPSA, a modular static analyzer. Our tool supports the Michelson semantic features, including inner calls to external contracts. It can prove the absence of runtime errors and infer invariants on the persistent storage over an unbounded number of calls. It is also being extended to prove high-level numerical and security properties. @InProceedings{SOAP22p36, author = {Guillaume Bau and Antoine Miné and Vincent Botbol and Mehdi Bouaziz}, title = {Abstract Interpretation of Michelson Smart-Contracts}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {36--43}, doi = {10.1145/3520313.3534660}, year = {2022}, } Publisher's Version Archive submitted (8.2 kB) |
|
Misu, Md Rakib Hossain |
SOAP '22: "ADA: A Tool for Visualizing ..."
ADA: A Tool for Visualizing the Architectural Overview of Open-Source Repositories
Md Rakib Hossain Misu, Aleksandar Saša Janjanin, Zhiqiang Bian, Valentin-Sebastian Burlacu, and Naum Anteski (University College London, UK) Writing highly maintainable and efficient software code is becoming increasingly difficult, especially while following the rapid, agile development process and working in a distributed team. One of the key indicators of that inefficient software design is a high degree of code coupling, which leads to unwanted side-effects during refactoring and acts as a burden during future development. To alleviate these problems, we developed a visualization tool, ADA, that statically analyzes an open-source repository and seeks to address the issue of code coupling by providing developers with a powerful graphic representation. ADA showcases the relationships and the degree of inter-connectivity between the classes. ADA will ultimately guide developers to instantly locate the coupled area and assist them in decoupling it. @InProceedings{SOAP22p30, author = {Md Rakib Hossain Misu and Aleksandar Saša Janjanin and Zhiqiang Bian and Valentin-Sebastian Burlacu and Naum Anteski}, title = {ADA: A Tool for Visualizing the Architectural Overview of Open-Source Repositories}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {30--35}, doi = {10.1145/3520313.3534659}, year = {2022}, } Publisher's Version |
|
Moscato, Mariano |
SOAP '22: "Towards an Implementation ..."
Towards an Implementation of Differential Dynamic Logic in PVS
J. Tanner Slagel, César Muñoz, Swee Balachandran, Mariano Moscato, Aaron Dutle, Paolo Masci, and Lauren White (NASA Langley Research Center, USA; National Institute of Aerospace, USA) This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, i.e., systems that employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and inference rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification of hybrid systems. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties. @InProceedings{SOAP22p44, author = {J. Tanner Slagel and César Muñoz and Swee Balachandran and Mariano Moscato and Aaron Dutle and Paolo Masci and Lauren White}, title = {Towards an Implementation of Differential Dynamic Logic in PVS}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {44--50}, doi = {10.1145/3520313.3534661}, year = {2022}, } Publisher's Version |
|
Muñoz, César |
SOAP '22: "Towards an Implementation ..."
Towards an Implementation of Differential Dynamic Logic in PVS
J. Tanner Slagel, César Muñoz, Swee Balachandran, Mariano Moscato, Aaron Dutle, Paolo Masci, and Lauren White (NASA Langley Research Center, USA; National Institute of Aerospace, USA) This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, i.e., systems that employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and inference rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification of hybrid systems. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties. @InProceedings{SOAP22p44, author = {J. Tanner Slagel and César Muñoz and Swee Balachandran and Mariano Moscato and Aaron Dutle and Paolo Masci and Lauren White}, title = {Towards an Implementation of Differential Dynamic Logic in PVS}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {44--50}, doi = {10.1145/3520313.3534661}, year = {2022}, } Publisher's Version |
|
Negrini, Luca |
SOAP '22: "Ensuring Determinism in Blockchain ..."
Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report
Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, and Enrico Talin (University of Verona, Italy; Corvallis, Italy; Commercio.network, Italy; University of Parma, Italy; Ca' Foscari University of Venice, Italy) Ensuring determinism is mandatory when writing blockchain software. When determinism is not met it can lead to serious implications in the blockchain network while compromising the software development, release, and patching processes. In the industrial context, it is widespread to adopt general-purpose languages, such as Go, for developing blockchain solutions. However, it is not surprising that non-deterministic behaviors may arise, being these programming languages not originally designed for blockchain purposes. In this paper, we present an experience report on ensuring determinism in blockchain software with GoLiSA, a static analyzer based on abstract interpretation for Go applications, in an industrial context. In particular, we ran GoLiSA on Commercio.network, a blockchain-based solution for exchanging electronic documents in a legally binding way. Thanks to GoLiSA, non-trivial bugs got detected and the analysis performed made it possible to identify the critical points where to apply the fixes. @InProceedings{SOAP22p23, author = {Luca Olivieri and Fabio Tagliaferro and Vincenzo Arceri and Marco Ruaro and Luca Negrini and Agostino Cortesi and Pietro Ferrara and Fausto Spoto and Enrico Talin}, title = {Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {23--29}, doi = {10.1145/3520313.3534658}, year = {2022}, } Publisher's Version |
|
Olivieri, Luca |
SOAP '22: "Ensuring Determinism in Blockchain ..."
Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report
Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, and Enrico Talin (University of Verona, Italy; Corvallis, Italy; Commercio.network, Italy; University of Parma, Italy; Ca' Foscari University of Venice, Italy) Ensuring determinism is mandatory when writing blockchain software. When determinism is not met it can lead to serious implications in the blockchain network while compromising the software development, release, and patching processes. In the industrial context, it is widespread to adopt general-purpose languages, such as Go, for developing blockchain solutions. However, it is not surprising that non-deterministic behaviors may arise, being these programming languages not originally designed for blockchain purposes. In this paper, we present an experience report on ensuring determinism in blockchain software with GoLiSA, a static analyzer based on abstract interpretation for Go applications, in an industrial context. In particular, we ran GoLiSA on Commercio.network, a blockchain-based solution for exchanging electronic documents in a legally binding way. Thanks to GoLiSA, non-trivial bugs got detected and the analysis performed made it possible to identify the critical points where to apply the fixes. @InProceedings{SOAP22p23, author = {Luca Olivieri and Fabio Tagliaferro and Vincenzo Arceri and Marco Ruaro and Luca Negrini and Agostino Cortesi and Pietro Ferrara and Fausto Spoto and Enrico Talin}, title = {Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {23--29}, doi = {10.1145/3520313.3534658}, year = {2022}, } Publisher's Version |
|
Ruaro, Marco |
SOAP '22: "Ensuring Determinism in Blockchain ..."
Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report
Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, and Enrico Talin (University of Verona, Italy; Corvallis, Italy; Commercio.network, Italy; University of Parma, Italy; Ca' Foscari University of Venice, Italy) Ensuring determinism is mandatory when writing blockchain software. When determinism is not met it can lead to serious implications in the blockchain network while compromising the software development, release, and patching processes. In the industrial context, it is widespread to adopt general-purpose languages, such as Go, for developing blockchain solutions. However, it is not surprising that non-deterministic behaviors may arise, being these programming languages not originally designed for blockchain purposes. In this paper, we present an experience report on ensuring determinism in blockchain software with GoLiSA, a static analyzer based on abstract interpretation for Go applications, in an industrial context. In particular, we ran GoLiSA on Commercio.network, a blockchain-based solution for exchanging electronic documents in a legally binding way. Thanks to GoLiSA, non-trivial bugs got detected and the analysis performed made it possible to identify the critical points where to apply the fixes. @InProceedings{SOAP22p23, author = {Luca Olivieri and Fabio Tagliaferro and Vincenzo Arceri and Marco Ruaro and Luca Negrini and Agostino Cortesi and Pietro Ferrara and Fausto Spoto and Enrico Talin}, title = {Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {23--29}, doi = {10.1145/3520313.3534658}, year = {2022}, } Publisher's Version |
|
Slagel, J. Tanner |
SOAP '22: "Towards an Implementation ..."
Towards an Implementation of Differential Dynamic Logic in PVS
J. Tanner Slagel, César Muñoz, Swee Balachandran, Mariano Moscato, Aaron Dutle, Paolo Masci, and Lauren White (NASA Langley Research Center, USA; National Institute of Aerospace, USA) This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, i.e., systems that employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and inference rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification of hybrid systems. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties. @InProceedings{SOAP22p44, author = {J. Tanner Slagel and César Muñoz and Swee Balachandran and Mariano Moscato and Aaron Dutle and Paolo Masci and Lauren White}, title = {Towards an Implementation of Differential Dynamic Logic in PVS}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {44--50}, doi = {10.1145/3520313.3534661}, year = {2022}, } Publisher's Version |
|
Spoto, Fausto |
SOAP '22: "Ensuring Determinism in Blockchain ..."
Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report
Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, and Enrico Talin (University of Verona, Italy; Corvallis, Italy; Commercio.network, Italy; University of Parma, Italy; Ca' Foscari University of Venice, Italy) Ensuring determinism is mandatory when writing blockchain software. When determinism is not met it can lead to serious implications in the blockchain network while compromising the software development, release, and patching processes. In the industrial context, it is widespread to adopt general-purpose languages, such as Go, for developing blockchain solutions. However, it is not surprising that non-deterministic behaviors may arise, being these programming languages not originally designed for blockchain purposes. In this paper, we present an experience report on ensuring determinism in blockchain software with GoLiSA, a static analyzer based on abstract interpretation for Go applications, in an industrial context. In particular, we ran GoLiSA on Commercio.network, a blockchain-based solution for exchanging electronic documents in a legally binding way. Thanks to GoLiSA, non-trivial bugs got detected and the analysis performed made it possible to identify the critical points where to apply the fixes. @InProceedings{SOAP22p23, author = {Luca Olivieri and Fabio Tagliaferro and Vincenzo Arceri and Marco Ruaro and Luca Negrini and Agostino Cortesi and Pietro Ferrara and Fausto Spoto and Enrico Talin}, title = {Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {23--29}, doi = {10.1145/3520313.3534658}, year = {2022}, } Publisher's Version |
|
Stojić, Milan |
SOAP '22: "Statically Detecting Data ..."
Statically Detecting Data Leakages in Data Science Code
Pavle Subotić, Uroš Bojanić, and Milan Stojić (Microsoft, Serbia) Data leakage is a well-known problem in machine learning. Data leakage occurs when information from outside the training dataset is used to create a model. This phenomenon renders a model excessively optimistic or even useless in the real world since the model tends to leverage greatly on the unfairly acquired information. To date, detection of data leakages occurs post-mortem using runtime methods. In this paper, we develop a static data leakage analysis to detect several instances of data leakages during development time. Our analysis is constructed to be lightweight so that it can be performed within interactive data science notebooks. We have integrated our analysis into the NBLyzer static analyzer framework and show its utility on real world benchmarks. To the best of our knowledge, we propose the first static detection of data science data leakages. @InProceedings{SOAP22p16, author = {Pavle Subotić and Uroš Bojanić and Milan Stojić}, title = {Statically Detecting Data Leakages in Data Science Code}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {16--22}, doi = {10.1145/3520313.3534657}, year = {2022}, } Publisher's Version |
|
Subotić, Pavle |
SOAP '22: "Statically Detecting Data ..."
Statically Detecting Data Leakages in Data Science Code
Pavle Subotić, Uroš Bojanić, and Milan Stojić (Microsoft, Serbia) Data leakage is a well-known problem in machine learning. Data leakage occurs when information from outside the training dataset is used to create a model. This phenomenon renders a model excessively optimistic or even useless in the real world since the model tends to leverage greatly on the unfairly acquired information. To date, detection of data leakages occurs post-mortem using runtime methods. In this paper, we develop a static data leakage analysis to detect several instances of data leakages during development time. Our analysis is constructed to be lightweight so that it can be performed within interactive data science notebooks. We have integrated our analysis into the NBLyzer static analyzer framework and show its utility on real world benchmarks. To the best of our knowledge, we propose the first static detection of data science data leakages. @InProceedings{SOAP22p16, author = {Pavle Subotić and Uroš Bojanić and Milan Stojić}, title = {Statically Detecting Data Leakages in Data Science Code}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {16--22}, doi = {10.1145/3520313.3534657}, year = {2022}, } Publisher's Version |
|
Tagliaferro, Fabio |
SOAP '22: "Ensuring Determinism in Blockchain ..."
Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report
Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, and Enrico Talin (University of Verona, Italy; Corvallis, Italy; Commercio.network, Italy; University of Parma, Italy; Ca' Foscari University of Venice, Italy) Ensuring determinism is mandatory when writing blockchain software. When determinism is not met it can lead to serious implications in the blockchain network while compromising the software development, release, and patching processes. In the industrial context, it is widespread to adopt general-purpose languages, such as Go, for developing blockchain solutions. However, it is not surprising that non-deterministic behaviors may arise, being these programming languages not originally designed for blockchain purposes. In this paper, we present an experience report on ensuring determinism in blockchain software with GoLiSA, a static analyzer based on abstract interpretation for Go applications, in an industrial context. In particular, we ran GoLiSA on Commercio.network, a blockchain-based solution for exchanging electronic documents in a legally binding way. Thanks to GoLiSA, non-trivial bugs got detected and the analysis performed made it possible to identify the critical points where to apply the fixes. @InProceedings{SOAP22p23, author = {Luca Olivieri and Fabio Tagliaferro and Vincenzo Arceri and Marco Ruaro and Luca Negrini and Agostino Cortesi and Pietro Ferrara and Fausto Spoto and Enrico Talin}, title = {Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {23--29}, doi = {10.1145/3520313.3534658}, year = {2022}, } Publisher's Version |
|
Talin, Enrico |
SOAP '22: "Ensuring Determinism in Blockchain ..."
Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report
Luca Olivieri, Fabio Tagliaferro, Vincenzo Arceri, Marco Ruaro, Luca Negrini, Agostino Cortesi, Pietro Ferrara, Fausto Spoto, and Enrico Talin (University of Verona, Italy; Corvallis, Italy; Commercio.network, Italy; University of Parma, Italy; Ca' Foscari University of Venice, Italy) Ensuring determinism is mandatory when writing blockchain software. When determinism is not met it can lead to serious implications in the blockchain network while compromising the software development, release, and patching processes. In the industrial context, it is widespread to adopt general-purpose languages, such as Go, for developing blockchain solutions. However, it is not surprising that non-deterministic behaviors may arise, being these programming languages not originally designed for blockchain purposes. In this paper, we present an experience report on ensuring determinism in blockchain software with GoLiSA, a static analyzer based on abstract interpretation for Go applications, in an industrial context. In particular, we ran GoLiSA on Commercio.network, a blockchain-based solution for exchanging electronic documents in a legally binding way. Thanks to GoLiSA, non-trivial bugs got detected and the analysis performed made it possible to identify the critical points where to apply the fixes. @InProceedings{SOAP22p23, author = {Luca Olivieri and Fabio Tagliaferro and Vincenzo Arceri and Marco Ruaro and Luca Negrini and Agostino Cortesi and Pietro Ferrara and Fausto Spoto and Enrico Talin}, title = {Ensuring Determinism in Blockchain Software with GoLiSA: An Industrial Experience Report}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {23--29}, doi = {10.1145/3520313.3534658}, year = {2022}, } Publisher's Version |
|
White, Lauren |
SOAP '22: "Towards an Implementation ..."
Towards an Implementation of Differential Dynamic Logic in PVS
J. Tanner Slagel, César Muñoz, Swee Balachandran, Mariano Moscato, Aaron Dutle, Paolo Masci, and Lauren White (NASA Langley Research Center, USA; National Institute of Aerospace, USA) This paper describes an ongoing effort to embed and verify differential dynamic logic (dL) in the Prototype Verification System (PVS). dL is a logic for specifying and formally reasoning about hybrid systems, i.e., systems that employ both continuous and discrete dynamics. There are several benefits of this effort. First, the embedding of dL in PVS offers an independent formal verification of the semantics and inference rules of dL. Second, the embedding is fully operational within PVS, giving PVS practitioners the ability to use dL in the formal specification and verification of hybrid systems. Third, the rich specification language, type system, and powerful interactive prover of PVS can be used on dL objects. In addition to the embedding and verification of dL, a custom extension for Visual Studio Code has been developed, so that a stylized dL syntax can be used to specify hybrid programs and their properties. @InProceedings{SOAP22p44, author = {J. Tanner Slagel and César Muñoz and Swee Balachandran and Mariano Moscato and Aaron Dutle and Paolo Masci and Lauren White}, title = {Towards an Implementation of Differential Dynamic Logic in PVS}, booktitle = {Proc.\ SOAP}, publisher = {ACM}, pages = {44--50}, doi = {10.1145/3520313.3534661}, year = {2022}, } Publisher's Version |
34 authors
proc time: 6.73