An Extended Account of Trace-relating Compiler Correctness and Secure Compilation

Compiler correctness, in its simplest form, is defined as the inclusion of the set of traces of the compiled program in the set of traces of the original program. This is equivalent to the preservation of all trace properties. Here, traces collect, for instance, the externally observable events of each execution. However, this definition requires the set of traces of the source and target languages to be the same, which is not the case when the languages are far apart or when observations are fine-grained. To overcome this issue, we study a generalized compiler correctness definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. We set out to understand what guarantees this generalized compiler correctness definition gives us when instantiated with a non-trivial relation on traces. When this trace relation is not equality, it is no longer possible to preserve the trace properties of the source program unchanged. Instead, we provide a generic characterization of the target trace property ensured by correctly compiling a program that satisfies a given source property, and dually, of the source trace property one is required to show to obtain a certain target property for the compiled code. We show that this view on compiler correctness can naturally account for undefined behavior, resource exhaustion, different source and target values, side channels, and various abstraction mismatches. Finally, we show that the same generalization also applies to many definitions of secure compilation, which characterize the protection of a compiled program linked against adversarial code.

A Temporal Logic for Asynchronous Hyperproperties

Hyperproperties are properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a trace property defines a set of traces, a hyperproperty defines a set of sets of traces. The temporal logics HyperLTL and HyperCTL* have been proposed to express hyperproperties. However, their semantics are synchronous in the sense that all traces proceed at the same speed and are evaluated at the same position. This precludes the use of these logics to analyze systems whose traces can proceed at different speeds and allow that different traces take stuttering steps independently. To solve this problem in this paper, we propose an asynchronous variant of HyperLTL. On the negative side, we show that the model-checking problem for this variant is undecidable. On the positive side, we identify a decidable fragment which covers a rich set of formulas with practical applications. We also propose two model-checking algorithms that reduce our problem to the HyperLTL model-checking problem in the synchronous semantics.

Trace-Relating Compiler Correctness and Secure Compilation

Compiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equivalent to the preservation of all trace properties. Here traces collect, for instance, the externally observable events of each execution. This definition requires, however, the set of traces of the source and target languages to be exactly the same, which is not the case when the languages are far apart or when observations are fine-grained. To overcome this issue, we study a generalized compiler correctness definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. We set out to understand what guarantees this generalized compiler correctness definition gives us when instantiated with a non-trivial relation on traces. When this trace relation is not equality, it is no longer possible to preserve the trace properties of the source program unchanged. Instead, we provide a generic characterization of the target trace property ensured by correctly compiling a program that satisfies a given source property, and dually, of the source trace property one is required to show in order to obtain a certain target property for the compiled code. We show that this view on compiler correctness can naturally account for undefined behavior, resource exhaustion, different source and target values, side-channels, and various abstraction mismatches. Finally, we show that the same generalization also applies to many secure compilation definitions, which characterize the protection of a compiled program against linked adversarial code.

PEMBATASAN TRANSAKSI TUNAI DI INDONESIA DALAM TINDAK PIDANA PENCUCIAN UANG

Combating crime is repressive, in the old paradigm insists on Follow the Suspect is more focused on the pursuit of the perpetrators. Unlike the case with the new paradigm that emphasizes the pursuit of money or the Follow the Money or trying to trace property derived from crime, which is then reconstructed where wealth and what criminal act that gave birth to such property. This approach is easier than with conventional approaches for money laundering is the weakest link of a crime. Pursuing the perpetrators of crimes are relatively more difficult, than the pursuit of crime. Pemberantasan kejahatan secara represif, dalam paradigma lama menekankan pada Follow the Suspect lebih menitikberatkan pada pengejaran para pelaku kejahatan. Berbeda halnya dengan paradigma baru yang lebih menekankan untuk mengejar uang atau Follow the Money atau berupaya melacak harta kekayaan yang berasal dari kejahatan, yang kemudian direkonstruksi dari mana kekayaan itu dan tindak pidana apa yang melahirkan kekayaan tersebut. Pendekatan ini lebih mudah dibandingkan dengan pendekatan konvensional karena pencucian uang adalah mata rantai paling lemah dari suatu kejahatan. Mengejar pelaku kejahatan relatif lebih sulit, dibandingkan dengan mengejar hasil kejahatan.