La programmation temps constant est utilisée pour produire des programmes immunisés contre les attaques temporelles. Cependant, cette discipline impose plusieurs contraintes au développeur de logiciels, ce qui rend la mise en œuvre complexe et les programmes résultants parfois plus lents. Nous proposons un nouveau mécanisme de protection spécialisé pour les systèmes embarqués qui est implémenté dans le matériel mais utilisable à partir du logiciel. Grâce à cette protection, les contraintes de la programmation temps constant peuvent être assouplies, ce qui rend cette discipline plus simple et permet de produire des programmes plus rapides. Cette protection fonctionne en verrouillant des parties de la mémoire dans le cache, de sorte que les accès vers ces parties de la mémoire soient protégés contre les attaques temporelles. Nous réutilisons les techniques de preuve utilisées pour certifier le compilateur CompCert. Dans notre cas, nous l'utilisons pour certifier qu'aucune attaque par cache ne peut exposer nos accès mémoire protégés. Nous montrons le gain de performance permis par notre nouvelle protection sur plusieurs algorithmes cryptographiques, et nous proposons une nouvelle méthode de tri rapide qui est temps constant grâce ce mécanisme de verrouillage du cache.