Formal modelling and analysis of behaviour grading within a peer-to-peer storage system

International audienceIn this paper, we extend a peer-to-peer based storage system in order to cope with malicious nodes. To do so, we introduce a grading system allowing peers to evaluate the outcome of their transactions with others, and consequently allowing to detect misbehaving peers. We evaluate this extension by two means. On the one hand, we have built a formal model of the system and used model-checking to verify whether malicious peers can be always detected or not. On the other hand, we have implemented the system and used simulation to assess malicious peers detection in realistic situations. Thanks to this analysis, we can guarantee that some attacks are necessarily detected while others remain undetected and, worse, may yield false positive (i.e., some peers are graded as being malicious while they are not). We propose solutions to improve this situation at the end of the paper