Abstract
The constant-time programming discipline is an effective countermeasure against timing attacks, which can lead to complete breaks of otherwise secure systems. However, adhering to constant-time programming is hard on its own, and extremely hard under additional efficiency and legacy constraints. This makes automated verification of constant-time code an essential component for building secure software. We propose a novel approach for verifying constant-time security of real-world code. Our approach is able to validate implementations that locally and intentionally violate the constant-time policy, when such violations are benign and leak no more information than the public outputs of the computation. Such implementations, which are used in cryptographic libraries to obtain important speedups or to comply with legacy APIs, would be declared insecure by all prior solutions. We implement our approach in a publicly available, cross-platform, and fully automated prototype, ct-verif, that leverages the SMACK and Boogie tools and verifies optimized LLVM implementations. We present verification results obtained over a wide range of constant-time components from the NaCl, OpenSSL, FourQ and other off-the-shelf libraries. The diversity and scale of our examples, as well as the fact that we deal with top-level APIs rather than being limited to low-level leaf functions, distinguishes ct-verif from prior tools. Our approach is based on a simple reduction of constant-time security of a program P to safety of a product program Q that simulates two executions of P. We formalize and verify the reduction for a core high-level language using the Coq proof assistant.

Abstract
This paper presents Enki, a web-based IDE that integrates several pedagogical tools designed to engage students in learning programming languages. Enki achieves this goal (1) by sequencing educational resources, either expository or evaluative, (2) by using gamification services to entice students to solve activities, (3) by promoting social interaction and (4) by helping students with activities, providing feedback on submitted solutions. The paper describes Enki, its concept and architecture, details its design and implementation, and covers also its validation.

Abstract
This paper proposes a calculational approach to prove properties of two well-known binary trees used to enumerate the rational numbers: the Stern-Brocot tree and the Eisenstein-Stern tree (also known as Calkin-Wilf tree). The calculational style of reasoning is enabled by a matrix formulation that is well-suited to naturally formulate path-based properties, since it provides a natural way to refer to paths in the trees. Three new properties are presented. First, we show that nodes with palindromic paths contain the same rational in both the Stern-Brocot and Eisenstein-Stern trees. Second, we show how certain numerators and denominators in these trees can be written as the sum of two squares x(2) and y(2), with the rational x/y appearing in specific paths. Finally, we show how we can construct Sierpifiski's triangle from these trees of rationals. (C) 2015 Published by Elsevier Inc.

Abstract
Prior to having available the High Dynamic Range (HDR) techniques, certain levels of luminance could only by captured by the human eye. Currently, HDR technology overcomes the limitations of conventional imaging technology (also referred as Low Dynamic Range or LDR) and allows the capture and delivery of contents that can match the dynamic range of the real world. However, the state of the art of HDR video focus mainly on conventional sized displays typical of TVs or PCs. As the usage of mobile devices for multimedia consumption is increasing considerably, there is a need for studying the impact of the viewing of HDR video on such devices. This will allow to take full advantage of HDR technology, creating a set of opportunities for the digital business as it allows, among others, the presentation of products in a much more efficient and captivating way. On this paper it is presented a study that evaluates the impact of the HDR video delivery on mobile devices and compares it with the impact of Low Dynamic Range (LDR) content. Results show that the delivery of HDR video on mobiles is possible without requiring much more resources when comparing the delivery of LDR video.

Abstract
Cloud-based storage services such as Dropbox, Google Drive and OneDrive are increasingly popular for storing enterprise data, and they have already become the de facto choice for cloud-based backup of hundreds of millions of regular users. Drawn by the wide range of services they provide, no upfront costs and 24/7 availability across all personal devices, customers are well-aware of the benefits that these solutions can bring. However, most users tend to forget-or worse ignore-some of the main drawbacks of such cloud-based services, namely in terms of privacy. Data entrusted to these providers can be leaked by hackers, disclosed upon request from a governmental agency's subpoena, or even accessed directly by the storage providers (e.g., for commercial benefits). While there exist solutions to prevent or alleviate these problems, they typically require direct intervention from the clients, like encrypting their data before storing it, and reduce the benefits provided such as easily sharing data between users. This practical experience report studies a wide range of security mechanisms that can be used atop standard cloud-based storage services. We present the details of our evaluation testbed and discuss the design choices that have driven its implementation. We evaluate several state-of-the-art techniques with varying security guarantees responding to user-assigned security and privacy criteria. Our results reveal the various trade-offs of the different techniques by means of representative workloads on top of industry-grade storage services.

Abstract
Technology for virtual reality has evolved at a fast pace and so is its affordability. Equipment such as head-mounted displays are now available for the average consumer at reasonable prices and this potentiates the use of contents such as video 360 in a more natural way. The purpose of this study was to measure the sense of presence and cybersickness comparing subjects by gender while experiencing a virtual reality application composed by type of VIDEO (360 video and 3D 360 video) using an head-mounted display. A Portuguese version of the Igroup Presence Questionnaire (IPQ) was used together with the Simulator Sickness Questionnaire (SSQ). The results have revealed that there are no significant differences across 2D and 3D videos in the sense of presence or cybersickness. © 2016 ACM.