Biblio

Software} maintainers employ reverse-engineered sequence diagrams to visually understand software behavior, especially when software documentation is absent or outdated. Much research has studied the adoption of reverse-engineered sequence diagrams to visualize program interactions. However, due to the forward-engineering nature of sequence diagrams, visualizing more complex programming scenarios can be challenging. In particular, sequence diagrams represent method invocations as unidirectional arrows. However, in practice, source code may contain compound method invocations that share values/objects implicitly. For example, method invocations can be nested, e.g., fun (foo ()), or chained, e.g., fun (). foo (). The standard notation of sequence diagrams does not have enough expressive power to precisely represent compound scenarios of method invocations. Understanding the flow of information between method invocations simplifies debugging, inspection, and exception handling operations for software maintainers. Despite the research invested to address the limitations of UML sequence diagrams, previous approaches fail to visualize compound scenarios of method invocations. In this paper, we propose sequence diagram extensions to enhance the visualization of (i) three widely used types of compound method invocations in practice (i.e., nested, chained, and recursive) and (ii) lifelines of objects returned from method invocations. We aim through our extensions to increase the level of abstraction and expressiveness of method invocation code. We develop a tool to reverse engineer compound method invocations and generate the corresponding extended sequence diagrams. We evaluate how our proposed extensions can improve the understandability of program interactions using a controlled experiment. We find that program interactions are significantly more comprehensible when visualized using our extensions.

Denial of Service (DoS) attacks have been a serious security concern, as no service is, in principle, protected against them. Although a Dolev-Yao intruder with unlimited resources can trivially render any service unavailable, DoS attacks do not necessarily have to be carried out by such (extremely) powerful intruders. It is useful in practice and more challenging for formal protocol verification to determine whether a service is vulnerable even to resource-bounded intruders that cannot generate or intercept arbitrary large volumes of traffic. This paper proposes a novel, more refined intruder model where the intruder can only consume at most some specified amount of resources in any given time window. Additionally, we propose protocol theories that may contain timeouts and specify service resource usage during protocol execution. In contrast to the existing resource-conscious protocol verification models, our model allows finer and more subtle analysis of DoS problems. We illustrate the power of our approach by representing a number of classes of DoS attacks, such as, Slow, Asymmetric and Amplification DoS attacks, exhausting different types of resources of the target, such as, number of workers, processing power, memory, and network bandwidth. We show that the proposed DoS problem is undecidable in general and is PSPACE-complete for the class of resource-bounded, balanced systems. Finally, we implemented our formal verification model in the rewriting logic tool Maude and analyzed a number of DoS attacks in Maude using Rewriting Modulo SMT in an automated fashion.