Attribute-based access control (ABAC) and relationship-based access control (ReBAC) are innovative access control methods that extend traditional models, including role-based access control (RBAC). This paper examines these models to suggest their application as a means of verifying the consent of a personal data subject. The objective is to apply these models in accordance with the General Data Protection Regulation (GDPR), which requires data owners to consent to the processing of their data for defined purposes, and ensure users utilize this data solely for those purposes. To validate this, we explore a benchmark proposed by NIST related to access control in a hospital setting, modifying it to assess data subject consent. From this case study, we deployed both access control approaches and subsequently compared their performance.

Cyber ranges are computer systems designed to create realistic cybersecurity scenarios for training purposes. It is essential to have a reliable evaluation process to determine whether users have achieved their objectives. User training involves a sequence of activities that are performed in a specific order to reach a particular goal. This article presents a cyber range implementation and puts forth an evaluation methodology that employs process mining to analyze training processes from different perspectives. The methodology is applied in a training session conducted in the cyber range.

In this paper we present the results of carrying out a security assessment of the FIWARE technology, by adopting an offensive perspective in the search of potential vulnerabilities involved in deployments of FIWARE components in certain architecture configurations. We consider a referential scenario that includes core components of a FIWARE platform. By experimenting in a locally controlled environment, it was possible to identify a series of security issues. Then, we put forward a threat model following the OWASP methodology that embodies several artifacts, namely, decomposition of the referential platform, a data flow diagram, a STRIDE threat modeling, attack analysis and the identification of attack objectives. We were able to implement attacks for three of the identified attack goals. The approach conducted for the referential platform was validated by performing an exploratory analysis of a real working and productive FIWARE platform, distinguishing different types of attacks that could be implemented, ending up with a set of recommendations in terms of components, architecture and access control.

Mimblewimble is a privacy-oriented cryptocurrency technology that provides security and scalability properties that distinguish it from other protocols. Mimblewimble’s cryptographic approach is based on Elliptic Curve Cryptography which allows verifying a transaction without revealing any information about the transactional amount or the parties involved. Mimblewimble combines Confidential transactions, CoinJoin, and cut-through to achieve a higher level of privacy, security, and scalability. In our previous work ([2], [26], [25]), we have presented and discussed these security properties and presented a model-driven verification approach in order to guarantee the correctness of the protocol implementations. In particular, we have proposed an idealized model that is essential to the described verification process. In that formal setting, we say that a transaction is valid if it is balanced, all output range proofs are valid and the kernel signature is valid for the excess. However, no formal and precise definition was given to the signature requirement. In this paper, we put forward an extension of our model to enable signatures. We specify a signature scheme that allows us to develop several properties and lemmas we have defined on our initial idealized model. The definition of a valid transaction is extended accordingly.

Since the beginning of 2020, COVID-19 has had a strong impact on the health of the world population. Tracing the contacts of infected people is one of the main strategies for controlling the pandemic. Given the high rates of contagion, which makes difficult an effective manual tracing, multiple initiatives arose for developing digital proximity tracing technologies. In this paper, we discuss in depth the security and personal data protection requirements that these technologies must satisfy, and we present an exhaustive and detailed list of the various applications that have been deployed globally. In particular, we identify potential threats that could undermine the satisfaction of the analyzed requirements, violating hegemonic personal data protection regulations.

Web applications are permanently being exposed to attacks that exploit their vulnerabilities. To detect and prevent misuse of the functionality provided by an application, it has become necessary to develop techniques that help discern between a valid user of the system and a malicious agent. In recent years, a technology that has been widely deployed to provide automated and non-invasive support for detecting web application attacks is Web Application Firewalls. In this work, we put forward and discuss the application of Process Mining techniques to detect deviations from the expected behavior of web applications. The objects of behavior analysis are logs generated by a widely deployed WAF called ModSecurity. We discuss experiments we have carried out applying our mining method on the well-known e-commerce platform Magento and using the ProM tool for the execution of the process mining techniques.

Web applications are permanently being exposed to attacks that exploit their vulnerabilities. In this work we investigate the application of machine learning techniques to leverage Web Application Firewalls (WAF)s, a technology that is used to detect and prevent attacks. We put forward an approach of complementary machine learning models, based on one-class classification and n-gram analysis, to enhance the detection and accuracy capabilities of MODSECURITY, an open source and widely used WAF. The results are promising and outperform MODSECURITY when configured with the OWASP Core Rule Set, the baseline configuration setting of a widely deployed, rule-based WAF technology.

Web applications are permanently being exposed to attacks that exploit their vulnerabilities. In this work we investigate the use of machine learning techniques to leverage the performance of Web Application Firewalls (WAFs), systems that are used to detect and prevent attacks. We propose a characterization of the problem by defining different scenarios depending if we have valid and/or attack data available for training. We also propose two solutions: first a multi-class approach for the scenario when valid and attack data is available; and second a one-class solution when only valid data is at hand. We present results using both approaches that outperform MODSECURITY configured with the OWASP Core Rule Set out of the box, which is the baseline configuration setting of a widely deployed WAF technology. We also propose a tagged dataset based on the DRUPAL content management framework.

This article reports on our experiences in applying formal methods to verify the security mechanisms of Android. We have developed a comprehensive formal specification of Android's permission model, which has been used to state and prove properties that establish expected behavior of the procedures that enforce the defined access control policy. We are also interested in providing guarantees concerning actual implementations of the mechanisms. Therefore we are following a verification approach that combines the use of idealized models on which fundamental properties are formally verified with testing of actual implementations using lightweight model-based techniques. We describe the formalized model, present security properties that have been verified using the Coq proof assistant and discuss a testing technique that relies on the use of certified algorithms.

Cache-based attacks are a class of side-channel attacks that are particularly effective in virtualized or cloud-based environments, where they have been used to recover secret keys from cryptographic implementations. One common approach to thwart cache-based attacks is to use constant-time implementations, i.e., which do not branch on secrets and do not perform memory accesses that depend on secrets. However, there is no rigorous proof that constant-time implementations are protected against concurrent cache-attacks in virtualization platforms with shared cache; moreover, many prominent implementations are not constant-time. An alternative approach is to rely on system-level mechanisms. One recent such mechanism is stealth memory, which provisions a small amount of private cache for programs to carry potentially leaking computations securely. Stealth memory induces a weak form of constant-time, called S-constant-time, which encompasses some widely used cryptographic implementations. However, there is no rigorous analysis of stealth memory and S-constant-time, and no tool support for checking if applications are S-constant-time.

This paper presents a Specialization Diploma in Computer Security (Diploma de Especialización en Seguridad Informática), defined in the context of the work of the Computer Security Group (GSI, Grupo de Seguridad Informática) of the Department of Computer Science (InCo, Instituto de Computación) at Facultad de Ingeniería, Universidad de la República, which is part of the course offerings by Centro de Posgrado y Actualización Profesional (CPAP). It describes the context in which it is developed, the objectives and structure of the curriculum, the teaching methodology used, and the educational tools.

Virtualization platforms allow multiple operating systems to run on the same hardware. One of their central goal is to provide strong isolation between guest operating systems, unfortunately, they are often vulnerable to practical side-channel attacks. Cache attacks are a common class of side-channel attacks that use the cache as a side channel. We formalize an idealized model of virtualization that features the cache and the Translation Look aside Buffer (TLB), and that provides an abstract treatment of cache-based side-channels. We then use the model for reasoning about cache-based attacks and countermeasures, and for proving that isolation between guest operating systems can be enforced by flushing the cache upon context switch. In addition, we show that virtualized platforms are transparent, i.e. a guest operating system cannot distinguish whether it executes alone or together with other guest operating systems on the platform. The models and proofs have been machine-checked in the Coqproof assistant.

The nature of computer crimes has systematically evolved with the progress of computer technologies. Due to the complexity of forensic investigations, the design of new techniques and tools for speeding up and automating tasks required by digital forensic processes has become a challenging task. In particular, the collection of (live) digital evidence is a delicate work that requires special care and proved investigator skills. This work presents a framework for the specification of collection procedures based on an extension of the OVAL language and describes a tool that has been implemented to automate the execution of those procedures.

In this work we put forward an algorithm for the mechanical verification of an extension of Martin-Löf's theory of types with dependent record types and subtyping. We first give a concise description of that theory and motivate its use for the formalization of algebraic constructions. Then we concentrate on the informal explanation and specification of a proof checker that we have implemented. The logical heart of this proof checker is a type checking algorithm for the forms of judgement of a particular formulation of the extended theory which incorporates a notion of parameter. The algorithm has been proven sound with respect to the latter calculus. We include a discussion on that proof in the present work.