\n \n \n
\n
\n\n \n \n \n \n \n \n Energy-Optimal Configurations for Single-Node HPC Applications.\n \n \n \n \n\n\n \n Silva, V. R. G.; Furtunato, A. F. A.; Georgiou, K.; Sakuyama, C. A. V.; Eder, K.; and Xavier-de-Souza, S.\n\n\n \n\n\n\n In
2019 International Conference on High Performance Computing Simulation (HPCS), pages 448–454, 2019. \n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{9188110,\r\n title = {Energy-Optimal Configurations for Single-Node HPC Applications},\r\n author = {Silva, Vitor R. G. and Furtunato, Alex F. A. and Georgiou, Kyriakos and Sakuyama, Carlos A. V. and Eder, Kerstin and Xavier-de-Souza, Samuel},\r\n year = 2019,\r\n booktitle = {2019 International Conference on High Performance Computing Simulation (HPCS)},\r\n pages = {448--454},\r\n doi = {10.1109/HPCS48598.2019.9188110},\r\n url = {http://arxiv.org/abs/1805.00998}\r\n}\r\n\r\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n A Time-, Energy- and Security-aware Coordination Approach.\n \n \n \n \n\n\n \n Roeder, J.; Rouxel, B.; Altmeyer, S.; and Grelck, C.\n\n\n \n\n\n\n In
10th International Workshop on Analysis Tools and Methodologies for Embedded Real-Time Systems (WATERS 2019), 31st Euromicro Conference on Real-Time Systems (ECRTS 2019), 2019. Euromicro, ECRTS\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{RoedRouxAltm+19b,\r\n title = {A Time-, Energy- and Security-aware Coordination Approach},\r\n author = {Julius Roeder and Benjamin Rouxel and Sebastian Altmeyer and Clemens Grelck},\r\n year = 2019,\r\n booktitle = {10th International Workshop on Analysis Tools and Methodologies for Embedded Real-Time Systems (WATERS 2019), 31st Euromicro Conference on Real-Time Systems (ECRTS 2019)},\r\n publisher = {Euromicro, ECRTS},\r\n url = {https://www.lexuor.net/publications/Rouxel_WATERS2019.pdf}\r\n}\r\n\r\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Favorable Adjustment of Periods for Reduced Hyperperiods in Real-Time Systems.\n \n \n \n \n\n\n \n Oehlert, D.; Luppold, A.; and Falk, H.\n\n\n \n\n\n\n In
Proceedings of the 22nd International Workshop on Software and Compilers for Embedded Systems, of
SCOPES '19, pages 82–85, New York, NY, USA, 2019. ACM\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{Oehlert:2019:SCOPES,\r\n title = {{Favorable Adjustment of Periods for Reduced Hyperperiods in Real-Time Systems}},\r\n author = {Oehlert, Dominic and Luppold, Arno and Falk, Heiko},\r\n year = 2019,\r\n booktitle = {Proceedings of the 22nd International Workshop on Software and Compilers for Embedded Systems},\r\n location = {Sankt Goar, Germany},\r\n publisher = {ACM},\r\n address = {New York, NY, USA},\r\n series = {SCOPES '19},\r\n pages = {82--85},\r\n doi = {10.1145/3323439.3323975},\r\n url = {https://tore.tuhh.de/bitstream/11420/2548/1/201905-scopes-oehlert.pdf},\r\n numpages = 4,\r\n keywords = {hyperperiod, real-time, integer linear programming}\r\n}\r\n\r\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Interdependent Multi-version Scheduling in Heterogeneous Energy-aware Embedded Systems.\n \n \n \n \n\n\n \n Roeder, J.; Rouxel, B.; Altmeyer, S.; and Grelck, C.\n\n\n \n\n\n\n In Rouxel, B.; and Paolillo, A., editor(s),
13th Junior Researcher Workshop on Real-Time Computing (JRWRTC 2019), part of the 27th International Conference on Real-Time Networks and Systems (RTNS 2019), Toulouse, France, pages 45–48, 2019. INP ENSEEIHT\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{RoedRouxAltm+19a,\r\n title = {Interdependent Multi-version Scheduling in Heterogeneous Energy-aware Embedded Systems},\r\n author = {Julius Roeder and Benjamin Rouxel and Sebastian Altmeyer and Clemens Grelck},\r\n year = 2019,\r\n booktitle = {13th Junior Researcher Workshop on Real-Time Computing (JRWRTC 2019), part of the 27th International Conference on Real-Time Networks and Systems (RTNS 2019), Toulouse, France},\r\n publisher = {INP ENSEEIHT},\r\n pages = {45--48},\r\n editor = {B. Rouxel and A. Paolillo},\r\n url = {https://hdl.handle.net/11245.1/fc811fd8-3eb7-4327-8ec0-370074b75b28}\r\n}\r\n\r\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Multi-Objective Optimization for the Compiler of Real-Time Systems based on Flower Pollination Algorithm.\n \n \n \n \n\n\n \n Jadhav, S.; and Falk, H.\n\n\n \n\n\n\n In
Proceedings of the 22nd International Workshop on Software and Compilers for Embedded Systems, of
SCOPES '19, pages 45–48, New York, NY, USA, 2019. ACM\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{Jadhav:2019:SCOPES,\r\n title = {{Multi-Objective Optimization for the Compiler of Real-Time Systems based on Flower Pollination Algorithm}},\r\n author = {Jadhav, Shashank and Falk, Heiko},\r\n year = 2019,\r\n booktitle = {Proceedings of the 22nd International Workshop on Software and Compilers for Embedded Systems},\r\n location = {Sankt Goar, Germany},\r\n publisher = {ACM},\r\n address = {New York, NY, USA},\r\n series = {SCOPES '19},\r\n pages = {45--48},\r\n doi = {10.1145/3323439.3323977},\r\n url = {https://tore.tuhh.de/bitstream/11420/2724/1/201905-scopes-jadhav.pdf},\r\n numpages = 4,\r\n keywords = {compiler, multi-objective, optimization, flower pollination algorithm}\r\n}\r\n\r\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Reasoning about non-functional properties using compiler intrinsic function annotations.\n \n \n \n \n\n\n \n Jadhav, S.; Roth, M.; Falk, H.; Brown, C.; and Barwell, A.\n\n\n \n\n\n\n In
Proceedings of the 13th Junior Researcher Workshop on Real-Time Computing, of
JRWRTC '19, pages 25–28, 2019. \n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{Jadhav:2019:JRWRTC,\r\n title = {{Reasoning about non-functional properties using compiler intrinsic function annotations}},\r\n author = {Jadhav, Shashank and Roth, Mikko and Falk, Heiko and Brown, Christopher and Barwell, Adam},\r\n year = 2019,\r\n booktitle = {Proceedings of the 13th Junior Researcher Workshop on Real-Time Computing},\r\n location = {Toulouse, France},\r\n series = {JRWRTC '19},\r\n pages = {25--28},\r\n doi = {10.15480/882.2545},\r\n url = {https://doi.org/10.15480/882.2545},\r\n numpages = 4,\r\n keywords = {Compilation, Annotations, Non-functional Properties, Function Inlining}\r\n}\r\n\r\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n A Trustworthy Framework for Resource-Aware Embedded Programming.\n \n \n \n \n\n\n \n Barwell, A. D.; and Brown, C.\n\n\n \n\n\n\n In
Proceedings of the 31st Symposium on Implementation and Application of Functional Languages, of
IFL '19, New York, NY, USA, 2019. Association for Computing Machinery\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{10.1145/3412932.3412944,\r\n title = {A Trustworthy Framework for Resource-Aware Embedded Programming},\r\n author = {Barwell, Adam D. and Brown, Christopher},\r\n year = 2019,\r\n booktitle = {Proceedings of the 31st Symposium on Implementation and Application of Functional Languages},\r\n location = {Singapore, Singapore},\r\n publisher = {Association for Computing Machinery},\r\n address = {New York, NY, USA},\r\n series = {IFL '19},\r\n doi = {10.1145/3412932.3412944},\r\n isbn = 9781450375627,\r\n url = {https://www.researchgate.net/profile/Christopher-Brown-89/publication/343416568_A_Trustworthy_Framework_for_Resource-Aware_Embedded_Programming/links/5f291a34299bf134049edae9/A-Trustworthy-Framework-for-Resource-Aware-Embedded-Programming.pdf},\r\n abstract = {Systems with non-functional requirements, such as Energy, Time and Security (ETS), are of increasing importance due to the proliferation of embedded devices with limited resources such as drones, wireless sensors, and tablet computers. Currently, however, there are little to no programmer supported methodologies or frameworks to allow them to reason about ETS properties in their source code. Drive is one such existing framework supporting the developer by lifting non-functional properties to the source-level through the Contract Specification Language (CSL), allowing non-functional properties to be first-class citizens, and supporting programmer-written code-level contracts to guarantee the non-functional specifications of the program are met. In this paper, we extend the Drive system by providing rigorous implementations of the underlying proof-engine, modeling the specification of the annotations and assertions from CSL for a representative subset of C, called Imp. We define both an improved abstract interpretation that automatically derives proofs of assertions, and define inference algorithms for the derivation of both abstract interpretations and the context over which the interpretation is indexed. We use the dependently-typed programming language, Idris, to give a formal definition, and implementation, of our abstract interpretation. Finally, we show our well-formed abstract interpretation over some representative exemplars demonstrating provable assertions of ETS.},\r\n articleno = 12,\r\n numpages = 12,\r\n keywords = {lightweight verification, idris, non-functional properties, dependent types, embedded systems}\r\n}\r\n\r\n
\n
\n\n\n
\n Systems with non-functional requirements, such as Energy, Time and Security (ETS), are of increasing importance due to the proliferation of embedded devices with limited resources such as drones, wireless sensors, and tablet computers. Currently, however, there are little to no programmer supported methodologies or frameworks to allow them to reason about ETS properties in their source code. Drive is one such existing framework supporting the developer by lifting non-functional properties to the source-level through the Contract Specification Language (CSL), allowing non-functional properties to be first-class citizens, and supporting programmer-written code-level contracts to guarantee the non-functional specifications of the program are met. In this paper, we extend the Drive system by providing rigorous implementations of the underlying proof-engine, modeling the specification of the annotations and assertions from CSL for a representative subset of C, called Imp. We define both an improved abstract interpretation that automatically derives proofs of assertions, and define inference algorithms for the derivation of both abstract interpretations and the context over which the interpretation is indexed. We use the dependently-typed programming language, Idris, to give a formal definition, and implementation, of our abstract interpretation. Finally, we show our well-formed abstract interpretation over some representative exemplars demonstrating provable assertions of ETS.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Cache-Timing Attack Detection and Prevention.\n \n \n \n \n\n\n \n Carré, S.; Facon, A.; Guilley, S.; Takarabt, S.; Schaub, A.; and Souissi, Y.\n\n\n \n\n\n\n In Polian, I.; and Stöttinger, M., editor(s),
Constructive Side-Channel Analysis and Secure Design, pages 13–21, Cham, 2019. Springer International Publishing\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{10.1007/978-3-030-16350-1_2,\r\n title = {Cache-Timing Attack Detection and Prevention},\r\n author = {Carr{\\'e}, S{\\'e}bastien and Facon, Adrien and Guilley, Sylvain and Takarabt, Sofiane and Schaub, Alexander and Souissi, Youssef},\r\n year = 2019,\r\n booktitle = {Constructive Side-Channel Analysis and Secure Design},\r\n publisher = {Springer International Publishing},\r\n address = {Cham},\r\n pages = {13--21},\r\n doi = {10.1007/978-3-030-16350-1_2},\r\n isbn = {978-3-030-16350-1},\r\n url = {https://hal-cnrs.archives-ouvertes.fr/hal-02915644},\r\n editor = {Polian, Ilia and St{\\"o}ttinger, Marc},\r\n abstract = {With the publication of Spectre {\\&} Meltdown attacks, cache-timing exploitation techniques have received a wealth of attention recently. On the one hand, it is now well understood which patterns in the source code create observable unbalances in terms of timing. On the other hand, some practical attacks have also been reported. But the exact relation between vulnerabilities and exploitations is not enough studied as of today. In this article, we put forward a methodology to characterize the leakage induced by a ``non-constant-time'' construct in the source code. This methodology allows us to recover known attacks and to warn about possible new ones, possibly devastating.}\r\n}\r\n\r\n
\n
\n\n\n
\n With the publication of Spectre & Meltdown attacks, cache-timing exploitation techniques have received a wealth of attention recently. On the one hand, it is now well understood which patterns in the source code create observable unbalances in terms of timing. On the other hand, some practical attacks have also been reported. But the exact relation between vulnerabilities and exploitations is not enough studied as of today. In this article, we put forward a methodology to characterize the leakage induced by a ``non-constant-time'' construct in the source code. This methodology allows us to recover known attacks and to warn about possible new ones, possibly devastating.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Cache-Timing Attacks Still Threaten IoT Devices.\n \n \n \n \n\n\n \n Takarabt, S.; Schaub, A.; Facon, A.; Guilley, S.; Sauvage, L.; Souissi, Y.; and Mathieu, Y.\n\n\n \n\n\n\n In Carlet, C.; Guilley, S.; Nitaj, A.; and Souidi, E. M., editor(s),
Codes, Cryptology and Information Security, pages 13–30, Cham, 2019. Springer International Publishing\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{10.1007/978-3-030-16458-4_2,\r\n title = {Cache-Timing Attacks Still Threaten IoT Devices},\r\n author = {Takarabt, Sofiane and Schaub, Alexander and Facon, Adrien and Guilley, Sylvain and Sauvage, Laurent and Souissi, Youssef and Mathieu, Yves},\r\n year = 2019,\r\n booktitle = {Codes, Cryptology and Information Security},\r\n publisher = {Springer International Publishing},\r\n address = {Cham},\r\n pages = {13--30},\r\n doi = {10.1007/978-3-030-16458-4_2},\r\n isbn = {978-3-030-16458-4},\r\n url = {https://hal-cnrs.archives-ouvertes.fr/hal-02319488},\r\n editor = {Carlet, Claude and Guilley, Sylvain and Nitaj, Abderrahmane and Souidi, El Mamoun},\r\n abstract = {Deployed widely and embedding sensitive data, The security of IoT devices depend on the reliability of cryptographic libraries to protect user information. However when implemented on real systems, cryptographic algorithms are vulnerable to side-channel attacks based on their execution behavior, which can be revealed by measurements of physical quantities such as timing or power consumption. Some countermeasures can be implemented in order to prevent those attacks. However those countermeasures are generally designed at high level description, and when implemented, some residual leakage may persist. In this article we propose a methodology to assess the robustness of the MbedTLS library against timing and cache-timing attacks. This comprehensive study of side-channel security allows us to identify the most frequent weaknesses in software cryptographic code and how those might be fixed. This methodology checks the whole source code, from the top level routines to low level primitives, that are used for the final application. We retrieve hundreds of lines of code that leak sensitive information.}\r\n}\r\n\r\n
\n
\n\n\n
\n Deployed widely and embedding sensitive data, The security of IoT devices depend on the reliability of cryptographic libraries to protect user information. However when implemented on real systems, cryptographic algorithms are vulnerable to side-channel attacks based on their execution behavior, which can be revealed by measurements of physical quantities such as timing or power consumption. Some countermeasures can be implemented in order to prevent those attacks. However those countermeasures are generally designed at high level description, and when implemented, some residual leakage may persist. In this article we propose a methodology to assess the robustness of the MbedTLS library against timing and cache-timing attacks. This comprehensive study of side-channel security allows us to identify the most frequent weaknesses in software cryptographic code and how those might be fixed. This methodology checks the whole source code, from the top level routines to low level primitives, that are used for the final application. We retrieve hundreds of lines of code that leak sensitive information.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Coarse-Grained Computation-Oriented Energy Modeling for Heterogeneous Parallel Embedded Systems.\n \n \n \n \n\n\n \n Seewald, A.; Schultz, U. P.; Ebeid, E.; and Midtiby, H. S.\n\n\n \n\n\n\n
International Journal of Parallel Programming, 49(2): 136–157. 2019.\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{seewald2019coarse,\r\n title = {Coarse-Grained Computation-Oriented Energy Modeling for Heterogeneous Parallel Embedded Systems},\r\n author = {Seewald, Adam and Schultz, Ulrik Pagh and Ebeid, Emad and Midtiby, Henrik Skov},\r\n year = 2019,\r\n journal = {International Journal of Parallel Programming},\r\n publisher = {Springer},\r\n volume = 49,\r\n number = 2,\r\n pages = {136--157},\r\n doi = {10.1007/s10766-019-00645-y},\r\n issn = {0885-7458},\r\n url = {https://adamseewald.cc/short/coarse2019}\r\n}\r\n\r\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Code-Inherent Traffic Shaping for Hard Real-Time Systems.\n \n \n \n \n\n\n \n Oehlert, D.; Saidi, S.; and Falk, H.\n\n\n \n\n\n\n
ACM Trans. Embed. Comput. Syst., 18(5s). October 2019.\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@article{10.1145/3358215,\r\n title = {Code-Inherent Traffic Shaping for Hard Real-Time Systems},\r\n author = {Oehlert, Dominic and Saidi, Selma and Falk, Heiko},\r\n year = 2019,\r\n month = oct,\r\n journal = {ACM Trans. Embed. Comput. Syst.},\r\n publisher = {Association for Computing Machinery},\r\n address = {New York, NY, USA},\r\n volume = 18,\r\n number = {5s},\r\n doi = {10.1145/3358215},\r\n issn = {1539-9087},\r\n url = {https://tore.tuhh.de/handle/11420/4381},\r\n issue_date = {October 2019},\r\n abstract = {Modern hard real-time systems evolved from isolated single-core architectures to complex multi-core architectures which are often connected in a distributed manner. With the increasing influence of interconnections in hard real-time systems, the access behavior to shared resources of single tasks or cores becomes a crucial factor for the system’s overall worst-case timing properties. Traffic shaping is a powerful technique to decrease contention in a network and deliver guarantees on network streams. In this paper we present a novel approach to automatically integrate a traffic shaping behavior into the code of a program for different traffic shaping profiles while being as least invasive as possible. As this approach is solely depending on modifying programs on a code-level, it does not rely on any additional hardware or operating system-based functions.We show how different traffic shaping profiles can be implemented into programs using a greedy heuristic and an evolutionary algorithm, as well as their influences on the modified programs. It is demonstrated that the presented approaches can be used to decrease worst-case execution times in multi-core systems and lower buffer requirements in distributed systems.},\r\n articleno = 108,\r\n numpages = 21,\r\n keywords = {traffic shaping, multi-core, Real-time, event arrival functions}\r\n}\r\n\r\n
\n
\n\n\n
\n Modern hard real-time systems evolved from isolated single-core architectures to complex multi-core architectures which are often connected in a distributed manner. With the increasing influence of interconnections in hard real-time systems, the access behavior to shared resources of single tasks or cores becomes a crucial factor for the system’s overall worst-case timing properties. Traffic shaping is a powerful technique to decrease contention in a network and deliver guarantees on network streams. In this paper we present a novel approach to automatically integrate a traffic shaping behavior into the code of a program for different traffic shaping profiles while being as least invasive as possible. As this approach is solely depending on modifying programs on a code-level, it does not rely on any additional hardware or operating system-based functions.We show how different traffic shaping profiles can be implemented into programs using a greedy heuristic and an evolutionary algorithm, as well as their influences on the modified programs. It is demonstrated that the presented approaches can be used to decrease worst-case execution times in multi-core systems and lower buffer requirements in distributed systems.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Component-based computation-energy modeling for embedded systems.\n \n \n \n \n\n\n \n Seewald, A.; Schultz, U. P.; Roeder, J.; Rouxel, B.; and Grelck, C.\n\n\n \n\n\n\n In
Proceedings Companion of the 2019 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity, pages 5–6, 2019. ACM\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{seewald2019component,\r\n title = {Component-based computation-energy modeling for embedded systems},\r\n author = {Seewald, Adam and Schultz, Ulrik Pagh and Roeder, Julius and Rouxel, Benjamin and Grelck, Clemens},\r\n year = 2019,\r\n booktitle = {Proceedings Companion of the 2019 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity},\r\n pages = {5--6},\r\n doi = {10.1145/3359061.3362775},\r\n url = {https://adamseewald.cc/short/component2019},\r\n organization = {ACM}\r\n}\r\n\r\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Fault Analysis Assisted by Simulation.\n \n \n \n \n\n\n \n Chibani, K.; Facon, A.; Guilley, S.; Marion, D.; Mathieu, Y.; Sauvage, L.; Souissi, Y.; and Takarabt, S.\n\n\n \n\n\n\n ,263–277. 2019.\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 19 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{Chibani2019,\r\n title = {Fault Analysis Assisted by Simulation},\r\n author = {Chibani, Kais and Facon, Adrien and Guilley, Sylvain and Marion, Damien and Mathieu, Yves and Sauvage, Laurent and Souissi, Youssef and Takarabt, Sofiane},\r\n year = 2019,\r\n booktitle = {Automated Methods in Cryptographic Fault Analysis},\r\n publisher = {Springer International Publishing},\r\n address = {Cham},\r\n pages = {263--277},\r\n doi = {10.1007/978-3-030-11333-9_12},\r\n isbn = {978-3-030-11333-9},\r\n url = {https://hal-cnrs.archives-ouvertes.fr/hal-02915671},\r\n editor = {Breier, Jakub and Hou, Xiaolu and Bhasin, Shivam}\r\n}\r\n\r\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Programming Heterogeneous Parallel machines using Refactoring and Monte-Carlo Tree Search.\n \n \n \n \n\n\n \n Brown, C.; Janjic, V.; and McCall, J.\n\n\n \n\n\n\n In
12th International Symposium on High-Level Parallel Programming and Applications (HLPP), 2019. \n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{brownhlpp2019,\r\n title = {Programming Heterogeneous Parallel machines using Refactoring and Monte-Carlo Tree Search},\r\n author = {Christopher Brown and Vladimir Janjic and John McCall},\r\n year = 2019,\r\n booktitle = {12th International Symposium on High-Level Parallel Programming and Applications (HLPP)},\r\n doi = {10.1007/s10766-020-00665-z},\r\n url = {https://doi.org/10.1007/s10766-020-00665-z}\r\n}\r\n\r\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Proof-Carrying Plans.\n \n \n \n \n\n\n \n Schwaab, C.; Komendantskaya, E.; Hill, A.; Farka, F.; Petrick, R. P. A.; Wells, J.; and Hammond, K.\n\n\n \n\n\n\n In Alferes, J. J.; and Johansson, M., editor(s),
Practical Aspects of Declarative Languages, pages 204–220, Cham, 2019. Springer International Publishing\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{10.1007/978-3-030-05998-9_13,\r\n title = {Proof-Carrying Plans},\r\n author = {Schwaab, Christopher and Komendantskaya, Ekaterina and Hill, Alasdair and Farka, Franti{\\v{s}}ek and Petrick, Ronald P. A. and Wells, Joe and Hammond, Kevin},\r\n year = 2019,\r\n booktitle = {Practical Aspects of Declarative Languages},\r\n publisher = {Springer International Publishing},\r\n address = {Cham},\r\n pages = {204--220},\r\n doi = {10.1007/978-3-030-05998-9_13},\r\n isbn = {978-3-030-05998-9},\r\n url = {https://research-repository.st-andrews.ac.uk/handle/10023/16855},\r\n editor = {Alferes, Jos{\\'e} J{\\'u}lio and Johansson, Moa},\r\n abstract = {It is becoming increasingly important to verify safety and security of AI applications. While declarative languages (of the kind found in automated planners and model checkers) are traditionally used for verifying AI systems, a big challenge is to design methods that generate verified executable programs. A good example of such a ``verification to implementation'' cycle is given by automated planning languages like PDDL, where plans are found via a model search in a declarative language, but then interpreted or compiled into executable code in an imperative language. In this paper, we show that this method can itself be verified. We present a formal framework and a prototype Agda implementation that represent PDDL plans as executable functions that inhabit types that are given by formulae describing planning problems. By exploiting the well-known Curry-Howard correspondence, type-checking then automatically ensures that the generated program corresponds precisely to the specification of the planning problem.}\r\n}\r\n\r\n
\n
\n\n\n
\n It is becoming increasingly important to verify safety and security of AI applications. While declarative languages (of the kind found in automated planners and model checkers) are traditionally used for verifying AI systems, a big challenge is to design methods that generate verified executable programs. A good example of such a ``verification to implementation'' cycle is given by automated planning languages like PDDL, where plans are found via a model search in a declarative language, but then interpreted or compiled into executable code in an imperative language. In this paper, we show that this method can itself be verified. We present a formal framework and a prototype Agda implementation that represent PDDL plans as executable functions that inhabit types that are given by formulae describing planning problems. By exploiting the well-known Curry-Howard correspondence, type-checking then automatically ensures that the generated program corresponds precisely to the specification of the planning problem.\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Refactoring for Introducing and Tuning Parallelism for Heterogeneous Multicore Machiens in Erlang.\n \n \n \n \n\n\n \n Brown, C.; Janjic, V.; Barwell, A.; and Hammond, K.\n\n\n \n\n\n\n In
Journal of Concurrency and Computation: Practice and Experience CCPE, 2019. \n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{DBLP:conf/padl/SchwaabKHFPWH19-refactoring,\r\n title = {Refactoring for Introducing and Tuning Parallelism for Heterogeneous Multicore Machiens in Erlang},\r\n author = {Christopher Brown and Vladimir Janjic and Adam Barwell and Kevin Hammond},\r\n year = 2019,\r\n booktitle = {Journal of Concurrency and Computation: Practice and Experience CCPE},\r\n doi = {10.1002/cpe.5420},\r\n url = {https://risweb.st-andrews.ac.uk/portal/en/researchoutput/refactoring-for-introducing-and-tuning-parallelism-for-heterogeneous-multicore-machines-in-erlang(f31ae458-56ad-48b8-9df9-132877165e0f).html}\r\n}\r\n\r\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Refactoring GrPPI: Generic Refactoring for Generic Parallelism in C++.\n \n \n \n \n\n\n \n Brown, C.; Janjic, V.; Barwell, A.; and Garcia, J. D.\n\n\n \n\n\n\n In
12th International Symposium on High-Level Parallel Programming and Applications, 2019. \n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{brownhlpp2019-2,\r\n title = {Refactoring GrPPI: Generic Refactoring for Generic Parallelism in C++},\r\n author = {Christopher Brown and Vladimir Janjic and Adam Barwell and Jose Daniel Garcia},\r\n year = 2019,\r\n booktitle = {12th International Symposium on High-Level Parallel Programming and Applications},\r\n doi = {10.1007/s10766-020-00667-x},\r\n url = {https://risweb.st-andrews.ac.uk/portal/en/researchoutput/refactoring-grppi(84dd2979-e2bf-456c-9991-73e3cd996a17).html}\r\n}\r\n\r\n
\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Security Evaluation Against Side-Channel Analysis at Compilation Time.\n \n \n \n \n\n\n \n Bruneau, N.; Christen, C.; Danger, J.; Facon, A.; and Guilley, S.\n\n\n \n\n\n\n In Gueye, C. T.; Persichetti, E.; Cayrel, P.; and Buchmann, J., editor(s),
Algebra, Codes and Cryptology, pages 129–148, Cham, 2019. Springer International Publishing\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@inproceedings{10.1007/978-3-030-36237-9_8,\r\n title = {Security Evaluation Against Side-Channel Analysis at Compilation Time},\r\n author = {Bruneau, Nicolas and Christen, Charles and Danger, Jean-Luc and Facon, Adrien and Guilley, Sylvain},\r\n year = 2019,\r\n booktitle = {Algebra, Codes and Cryptology},\r\n publisher = {Springer International Publishing},\r\n address = {Cham},\r\n pages = {129--148},\r\n doi = {10.1007/978-3-030-36237-9_8},\r\n isbn = {978-3-030-36237-9},\r\n url = {https://hal-cnrs.archives-ouvertes.fr/hal-02915643},\r\n editor = {Gueye, Cheikh Thiecoumba and Persichetti, Edoardo and Cayrel, Pierre-Louis and Buchmann, Johannes},\r\n abstract = {Masking countermeasure is implemented to thwart side-channel attacks. The maturity of high-order masking schemes has reached the level where the concepts are sound and proven. For instance, Rivain and Prouff proposed a full-fledged AES at CHES 2010. Some non-trivial fixes regarding refresh functions were needed though. Now, industry is adopting such solutions, and for the sake of both quality and certification requirements, masked cryptographic code shall be checked for correctness using the same model as that of the theoretical protection rationale (for instance the probing leakage model).}\r\n}\r\n\r\n
\n
\n\n\n
\n Masking countermeasure is implemented to thwart side-channel attacks. The maturity of high-order masking schemes has reached the level where the concepts are sound and proven. For instance, Rivain and Prouff proposed a full-fledged AES at CHES 2010. Some non-trivial fixes regarding refresh functions were needed though. Now, industry is adopting such solutions, and for the sake of both quality and certification requirements, masked cryptographic code shall be checked for correctness using the same model as that of the theoretical protection rationale (for instance the probing leakage model).\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Type-Driven Verification of Non-Functional Properties.\n \n \n \n \n\n\n \n Brown, C.; Barwell, A. D.; Marquer, Y.; Minh, C.; and Zendra, O.\n\n\n \n\n\n\n In
Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, of
PPDP '19, New York, NY, USA, 2019. Association for Computing Machinery\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n \n \n abstract \n \n\n \n \n \n 9 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{10.1145/3354166.3354171,\r\n title = {Type-Driven Verification of Non-Functional Properties},\r\n author = {Brown, Christopher and Barwell, Adam D. and Marquer, Yoann and Minh, C\\'{e}line and Zendra, Olivier},\r\n year = 2019,\r\n booktitle = {Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming},\r\n location = {Porto, Portugal},\r\n publisher = {Association for Computing Machinery},\r\n address = {New York, NY, USA},\r\n series = {PPDP '19},\r\n doi = {10.1145/3354166.3354171},\r\n isbn = 9781450372497,\r\n url = {https://hal.inria.fr/hal-02314723/document},\r\n abstract = {Energy, Time and Security (ETS) properties of programs are becoming increasingly prioritised by developers, especially where applications are running on ETS sensitive systems, such as embedded devices or the Internet of Things. Moreover, developers currently lack tools and language properties to allow them to reason about ETS. In this paper, we introduce a new contract specification framework, called Drive, which allows a developer to reason about ETS or other non-functional properties of their programs as first-class properties of the language. Furthermore, we introduce a contract specification language, allowing developers to reason about these first-class ETS properties by expressing contracts that are proved correct by an underlying formal type system. Finally, we show our contract framework over a number of representable examples, demonstrating provable worst-case ETS properties.},\r\n articleno = 6,\r\n numpages = 15,\r\n keywords = {contracts, energy, verification, non-functional properties, proofs, security, time, C, IDRIS}\r\n}\r\n\r\n
\n
\n\n\n
\n Energy, Time and Security (ETS) properties of programs are becoming increasingly prioritised by developers, especially where applications are running on ETS sensitive systems, such as embedded devices or the Internet of Things. Moreover, developers currently lack tools and language properties to allow them to reason about ETS. In this paper, we introduce a new contract specification framework, called Drive, which allows a developer to reason about ETS or other non-functional properties of their programs as first-class properties of the language. Furthermore, we introduce a contract specification language, allowing developers to reason about these first-class ETS properties by expressing contracts that are proved correct by an underlying formal type system. Finally, we show our contract framework over a number of representable examples, demonstrating provable worst-case ETS properties.\n
\n\n\n
\n\n\n\n\n\n