Journal of Computer Security - Volume 26, issue 3

Authors: Diao, Wenrui | Liu, Rui | Liu, Xiangyu | Zhou, Zhe | Li, Zhou | Zhang, Kehuan

Article Type: Research Article

Abstract: Input Method Editor (IME) is an indispensable component on current smartphones. With its assistance, the number of key presses is reduced, and non-Latin characters could be inputted. Furthermore, modern IMEs integrate several personalized features like reordering suggestion lists and predicting the next words based on user’s input history. Such optimization improves the user experience but turns the IME dictionary into a pool of user privacy. Previous works have discussed the privacy risks coming from malicious IMEs. Indeed, they could cause security and privacy issues if installed by common users, but their impact is limited as the majority of IMEs are …well-behaved. However, whether legitimate IMEs are bullet-proof is not answered before. In this paper, we make the first attempt to study the security implications of IME personalization and the back-end infrastructure on Android devices. In the end, we identify a critical vulnerability lying under the Android KeyEvent processing framework, which can be exploited to launch cross-app KeyEvent injection (CAKI) attack and bypass the app-isolation mechanism. By abusing such design flaw, an adversary can harvest entries from the personalized user dictionary of IME through an ostensibly innocuous app only asking for common permissions. Our evaluation over a broad spectrum of Android OSes, devices, and IMEs suggests such issue should be fixed immediately. All Android versions we examined (from very old 2.3.4 to the latest 6.0.1) and most IME apps we surveyed (11 out of 18) are vulnerable. User’s private information, like contact names, location, etc., can be easily exfiltrated. Up to hundreds of millions of mobile users are under this threat. To mitigate this security issue, we propose a practical defense mechanism which augments the existing KeyEvent processing framework without forcing any change to IME apps. Show more

Keywords: Android, smart IME, privacy leakage, system flaw

DOI: 10.3233/JCS-16909

Citation: Journal of Computer Security, vol. 26, no. 3, pp. 283-309, 2018

Authors: Shirvanian, Maliheh | Saxena, Nitesh | Mukhopadhyay, Dibya

Article Type: Research Article

Abstract: Establishing secure voice, video and text over Internet (VoIP) communications is a crucial task necessary to prevent eavesdropping and man-in-the-middle attacks. The traditional means of secure session establishment (e.g., those relying upon PKI or KDC) require a dedicated infrastructure and may impose unwanted trust onto third-parties. “Crypto Phones” (popular instances such as PGPfone and Zfone), in contrast, provide a purely peer-to-peer user-centric secure mechanism claiming to completely address the problem of wiretapping. The secure association mechanism in Crypto Phones is based on cryptographic protocols employing Short Authenticated Strings (SAS) validated over the voice medium. The security of Crypto Phones …crucially relies on the assumption that the voice channel, over which SAS is validated, provides the properties of integrity and source authentication. In this paper, we challenge this assumption, and report on automated SAS voice imitation man-in-the-middle attacks that can compromise the security of Crypto Phones in both two-party and multi-party settings, even if users pay due diligence and even if an automated software (voice biometrics systems) is used to detect voice manipulation. The first attack, called the short voice reordering attack , builds arbitrary SAS strings in a victim’s voice by reordering previously eavesdropped SAS strings spoken by the victim. The second attack, called the short voice morphing attack , builds arbitrary SAS strings in a victim’s voice from a few previously eavesdropped sentences (less than 3 minutes) spoken by the victim. We design and implement our attacks using off-the-shelf speech recognition/synthesis tools, and comprehensively evaluate them with respect to both manual detection (based on a user study with 30 participants) and automated detection via a speaker verification tool. The results demonstrate the effectiveness of our attacks against three prominent forms of SAS encodings: numbers , PGP word lists and Madlib sentences. These attacks can be used by a wiretapper to compromise the confidentiality and privacy of Crypto Phones voice, video and text communications (plus authenticity in case of text conversations). Show more

Keywords: VoIP Security, Crypto Phone, End-to-End Encrypted VoIP, SAS protocols, voice morphing attack, voice biometrics

DOI: 10.3233/JCS-17970

Citation: Journal of Computer Security, vol. 26, no. 3, pp. 311-333, 2018

Authors: Bischof, Simon | Breitner, Joachim | Graf, Jürgen | Hecker, Martin | Mohr, Martin | Snelting, Gregor

Article Type: Research Article

Abstract: We present a new algorithm, together with a full soundness proof, which guarantees probabilistic noninterference (PN) for concurrent programs. The algorithm follows the “low-deterministic security” (LSOD) approach, but for the first time allows general low-nondeterminism as long as PN is not violated. The algorithm is based on the earlier observation by Giffhorn and Snelting that low-nondeterminism is secure as long as it is not influenced by high events [International Journal of Information Security 14 (2015 ) 263–287]. It uses a new system of classification flow equations in multi-threaded programs, together with inter-thread/interprocedural dominators. Compared to LSOD, …precision is boosted and false alarms are minimized. We explain details of the new algorithm and its soundness proof. The algorithm is integrated into the JOANA software security tool, and can handle full Java with arbitrary threads. We apply JOANA to a multi-threaded e-voting system, and show how the algorithm eliminates false alarms. We thus demonstrate that low-deterministic security is a highly precise and practically mature software security analysis method. Show more

Keywords: Software security, information flow control, probabilistic noninterference, program analysis

DOI: 10.3233/JCS-17984

Citation: Journal of Computer Security, vol. 26, no. 3, pp. 335-366, 2018

Authors: Blanchet, Bruno | Smyth, Ben

Article Type: Research Article

Abstract: Observational equivalence allows us to study important security properties such as anonymity. Unfortunately, the difficulty of proving observational equivalence hinders analysis. Blanchet, Abadi & Fournet simplify its proof by introducing a sufficient condition for observational equivalence, called diff-equivalence, which is a reachability condition that can be proved automatically by ProVerif. However, diff-equivalence is a very strong condition, which often does not hold even if observational equivalence does. In particular, when proving equivalence between processes that contain several parallel components, e.g., P ∣ Q and P ′ ∣ Q ′ …, diff-equivalence requires that P is equivalent to P ′ and Q is equivalent to Q ′ . To relax this constraint, Delaune, Ryan & Smyth introduced the idea of swapping data between parallel processes P ′ and Q ′ at synchronisation points, without proving its soundness. We extend their work by formalising the semantics of synchronisation, formalising the definition of swapping, and proving its soundness. We also relax some restrictions they had on the processes to which swapping can be applied. Moreover, we have implemented our results in ProVerif. Hence, we extend the class of equivalences that can be proved automatically. We showcase our results by analysing privacy in election schemes by Fujioka, Okamoto & Ohta, Lee et al. , and Juels, Catalano & Jakobsson, and in the vehicular ad-hoc network by Freudiger et al . Show more

Keywords: Applied pi calculus, automated reasoning, ballot secrecy, barrier synchronisation, equivalence, e-voting, privacy, receipt-freeness

DOI: 10.3233/JCS-171013

Citation: Journal of Computer Security, vol. 26, no. 3, pp. 367-422, 2018